diff options
| author |  qadeer <unknown> | 2010-11-27 08:31:52 +0000 |
|---|---|---|
| committer | qadeer <unknown> | 2010-11-27 08:31:52 +0000 |
| commit | e737198c1dd35f3fa460d346bda346f2e37799a4 (patch) | |
| tree | cc9aacd45edfd19bf7c86a847d5396653d942fef /Source/Provers/Z3api/ContextLayer.cs | |
| parent | 3476c4e0ca9125236330dbb13d976110544e3e68 (diff) | |
changed the procedure Check so that the conflict clause is blocked only when more than one counterexample is needed.
Diffstat (limited to 'Source/Provers/Z3api/ContextLayer.cs')
| -rw-r--r-- | Source/Provers/Z3api/ContextLayer.cs | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs index 9109e755..c444e8a1 100644 --- a/Source/Provers/Z3api/ContextLayer.cs +++ b/Source/Provers/Z3api/ContextLayer.cs @@ -90,7 +90,6 @@ namespace Microsoft.Boogie.Z3 string GetDeclName(Z3ConstDeclAst constDeclAst);
Z3PatternAst MakePattern(List<Z3TermAst> exprs);
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);
- List<string> BuildConflictClause(Z3LabeledLiterals relevantLabels);
ProverInterface.Outcome Check(out List<Z3ErrorModelAndLabels> boogieErrors);
void TypeCheckBool(Z3TermAst t);
void TypeCheckInt(Z3TermAst t);
|