summaryrefslogtreecommitdiff
path: root/Source/Provers/Z3api/StubContext.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Provers/Z3api/StubContext.cs')
-rw-r--r--Source/Provers/Z3api/StubContext.cs7
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>();