From 9974e2b281fb521f516a02c7313ef83256e09c38 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Tue, 26 Jun 2012 19:19:24 +0200
Subject: [PATCH] waypoint and @main can be used with standard leon
---
src/main/scala/leon/FairZ3Solver.scala | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 8ec0984ee..2a981382e 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -963,6 +963,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
z3Vars = z3Vars - i
rb
}
+ case Waypoint(_, e) => rec(e)
case e @ Error(_) => {
val tpe = e.getType
val newAST = z3.mkFreshConst("errorValue", typeToSort(tpe))
--
GitLab