From c57ef72622ef4bfd23dd42c656582bf0f778e6ee Mon Sep 17 00:00:00 2001
From: akashlal <akashl@AKASHL-LT.fareast.corp.microsoft.com>
Date: Sat, 20 Jun 2015 09:18:47 -0700
Subject: Fix for reading fixpoint back into boogie exprs

---
 Source/Provers/SMTLib/ProverInterface.cs | 22 +++++++++-------------
 1 file changed, 9 insertions(+), 13 deletions(-)

(limited to 'Source')

diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index 7e7f0cf6..0ff2efa7 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -597,7 +597,10 @@ namespace Microsoft.Boogie.SMTLib
 				if(declHandler.var_map.ContainsKey(name))
 					return declHandler.var_map[name];
 				HandleProverError ("Prover error: unknown symbol:" + name);
-				throw new BadExprFromProver ();
+				//throw new BadExprFromProver ();
+                var v = gen.Variable(name, Type.Int);
+                bound.Add(name, v);
+                return v;
 			}
 			ArgGetter g = i => SExprToVCExpr (e [i], bound);
 			ArgsGetter ga = () => e.Arguments.Select (x => SExprToVCExpr (x, bound)).ToArray ();
@@ -612,10 +615,11 @@ namespace Microsoft.Boogie.SMTLib
                 {
                     var binds = e.Arguments[0];
                     var vcbinds = new List<VCExprVar>();
+                    var bound_copy = new Dictionary<string, VCExpr>(bound);
                     for (int i = 0; i < binds.Arguments.Count(); i++)
                     {
                         var bind = binds.Arguments[i];
-                        var symb = bind.Name;
+                        var symb = StripCruft(bind.Name);
                         var vcv = SExprToVar(bind);
                         vcbinds.Add(vcv);
                         bound[symb] = vcv;
@@ -625,12 +629,7 @@ namespace Microsoft.Boogie.SMTLib
                         body = gen.Forall(vcbinds, new List<VCTrigger>(), body);
                     else
                         body = gen.Exists(vcbinds, new List<VCTrigger>(), body);
-                    for (int i = 0; i < binds.Arguments.Count(); i++)
-                    {
-                        var bind = binds.Arguments[i];
-                        var symb = bind.Name;
-                        bound.Remove(symb);
-                    }
+                    bound = bound_copy;
                     return body;
                 }
 			case "-" : // have to deal with unary case
@@ -650,6 +649,7 @@ namespace Microsoft.Boogie.SMTLib
 				bool expand_lets = true;
 				var binds = e.Arguments[0];
 				var vcbinds = new List<VCExprLetBinding>();
+                var bound_copy = new Dictionary<string, VCExpr>(bound);
 				for(int i = 0; i < binds.Arguments.Count(); i++){
 					var bind = binds.Arguments[i];
 					var symb = bind.Name;
@@ -663,11 +663,7 @@ namespace Microsoft.Boogie.SMTLib
 				var body = g(1); 
 				if(!expand_lets)
 					body = gen.Let(vcbinds,body);
-				for(int i = 0; i < binds.Arguments.Count(); i++){
-					var bind = binds.Arguments[i];
-					var symb = bind.Name;
-					bound.Remove (symb);
-				}
+                bound = bound_copy;
                 return body;
 			}
 				
-- 
cgit v1.2.3