BeginCheck now adds context.Axioms as well as the conjecture to the context.

Also started using the new quantifier api.

1 files changed, 2 insertions, 5 deletions

diff --git a/Source/Provers/Z3api/StubContext.cs b/Source/Provers/Z3api/StubContext.cs
index ade8cad0..17435e14 100644
--- a/Source/Provers/Z3api/StubContext.cs
+++ b/Source/Provers/Z3api/StubContext.cs
@@ -28,11 +28,8 @@ namespace Microsoft.Boogie.Z3 {
     public Z3PatternAst MakePattern(List<Z3TermAst> exprs) {

       return new Z3StubPatternAst();

     }

-    public Z3TermAst MakeForall(uint weight, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body) {

-      return new Z3StubTermAst();

-    }

-    public Z3TermAst MakeExists(uint weight, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body) {

-      return new Z3StubTermAst();

+    public Z3TermAst MakeQuantifier(bool isForall, uint weight, string qid, int skolemid, List<string> varNames, List<Type> boogieTypes, List<Z3PatternAst> patterns, List<Z3TermAst> no_patterns, Z3TermAst body) {

+        return new Z3StubTermAst();

     }

     public List<string> BuildConflictClause(Z3LabeledLiterals relevantLabels) {

       return new List<string>();