Some changes to support expanded use of z3api.

Should not affect function
of other provers. There is an option added in Check.cs to  allow creation
of a Checker with a user-specified ProverContext. Also, some extension of
z3api prover context to support conversion of Z3 formulas back to VCExpr.
Finally, some experimental code, not enabled, to allow conversion of loops to
recursion with "head recursion" rather than "tail recursion" (i.e., recursive
call before loop body rather than after).

1 files changed, 2 insertions, 2 deletions

diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs
index 149a23f1..0605a854 100644
--- a/Source/Provers/Z3api/VCExprVisitor.cs
+++ b/Source/Provers/Z3api/VCExprVisitor.cs
@@ -188,7 +188,7 @@ namespace Microsoft.Boogie.Z3
             else

             {

                 string varName = namer.GetName(node, node.Name);

-                return cm.GetConstant(varName, node.Type);

+                return cm.GetConstant(varName, node.Type,node);

             }

         }

 

@@ -252,7 +252,7 @@ namespace Microsoft.Boogie.Z3
         private Term MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Pattern> patterns, List<Term> no_patterns, Term body) {

           List<Term> bound = new List<Term>();

           for (int i = 0; i < varNames.Count; i++) {

-            Term t = cm.GetConstant(varNames[i], boogieTypes[i]);

+            Term t = cm.GetConstant(varNames[i], boogieTypes[i], null);

             bound.Add(t);

           }