From c54abbddd2d8c51dc71d936aae5e6238e14366bb Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 2 May 2016 16:32:11 +0200
Subject: [PATCH] Simplifier should handle negative Asserts
---
.../leon/purescala/SimplifierWithPaths.scala | 16 ++++++++--------
1 file changed, 8 insertions(+), 8 deletions(-)
diff --git a/src/main/scala/leon/purescala/SimplifierWithPaths.scala b/src/main/scala/leon/purescala/SimplifierWithPaths.scala
index ad56da7f4..4b64e468e 100644
--- a/src/main/scala/leon/purescala/SimplifierWithPaths.scala
+++ b/src/main/scala/leon/purescala/SimplifierWithPaths.scala
@@ -54,14 +54,11 @@ class SimplifierWithPaths(sf: SolverFactory[Solver], val initPath: Path = Path.e
case Require(pre, body) if impliedBy(pre, path) =>
body
- case IfExpr(cond, thenn, elze) =>
- if (impliedBy(cond, path)) {
- rec(thenn, path)
- } else if (contradictedBy(cond, path)) {
- rec(elze, path)
- } else {
- super.rec(e, path)
- }
+ case IfExpr(cond, thenn, _) if impliedBy(cond, path) =>
+ rec(thenn, path)
+
+ case IfExpr(cond, _, elze ) if contradictedBy(cond, path) =>
+ rec(elze, path)
case And(e +: _) if contradictedBy(e, path) =>
BooleanLiteral(false).copiedFrom(e)
@@ -127,6 +124,9 @@ class SimplifierWithPaths(sf: SolverFactory[Solver], val initPath: Path = Path.e
case a @ Assert(pred, _, body) if impliedBy(pred, path) =>
body
+ case a @ Assert(pred, msg, body) if contradictedBy(pred, path) =>
+ Error(body.getType, s"Assertion failed: $msg").copiedFrom(a)
+
case b if b.getType == BooleanType && impliedBy(b, path) =>
BooleanLiteral(true).copiedFrom(b)
--
GitLab