From c0b4ac13b4dc3b78e223e2e4aeff6fe87958320a Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 29 Jun 2015 14:29:53 +0200
Subject: [PATCH] Fix Asserts in VCs in fairz3
---
src/main/scala/leon/solvers/templates/TemplateGenerator.scala | 2 +-
src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala | 3 +++
2 files changed, 4 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index 61693206b..fd3af5c50 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -171,7 +171,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
rec(pathVar, body)
case e @ Ensuring(_, _) =>
- rec(pathVar, e.toAssert)
+ rec(pathVar, e.toAssert)
case l @ Let(i, e : Lambda, b) =>
val re = rec(pathVar, e) // guaranteed variable!
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 3959e2265..321f1234a 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -361,6 +361,9 @@ trait AbstractZ3Solver
}
case Waypoint(_, e, _) => rec(e)
+ case a @ Assert(cond, err, body) =>
+ rec(IfExpr(cond, body, Error(a.getType, err.getOrElse("Assertion failed")).setPos(a.getPos)).setPos(a.getPos))
+
case e @ Error(tpe, _) => {
val newAST = z3.mkFreshConst("errorValue", typeToSort(tpe))
// Might introduce dupplicates (e), but no worries here
--
GitLab