From 953ec3159e60ffdf4e52380408517c8029a5a4ef Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Sun, 22 Nov 2015 20:09:19 +0100
Subject: [PATCH] Support for global variables that are defined but may not in
z3vars
---
.../leon/solvers/z3/AbstractZ3Solver.scala | 17 ++++++++++++-----
1 file changed, 12 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 9a06cff26..d936a4e3a 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -309,12 +309,19 @@ trait AbstractZ3Solver extends Solver {
newAST
}
case v @ Variable(id) => z3Vars.get(id) match {
- case Some(ast) => ast
+ case Some(ast) =>
+ ast
case None => {
- val newAST = z3.mkFreshConst(id.uniqueName, typeToSort(v.getType))
- z3Vars = z3Vars + (id -> newAST)
- variables += (v -> newAST)
- newAST
+ variables.getB(v) match {
+ case Some(ast) =>
+ ast
+
+ case None =>
+ val newAST = z3.mkFreshConst(id.uniqueName, typeToSort(v.getType))
+ z3Vars = z3Vars + (id -> newAST)
+ variables += (v -> newAST)
+ newAST
+ }
}
}
--
GitLab