diff options
| author |  qadeer <unknown> | 2010-08-27 05:07:49 +0000 |
|---|---|---|
| committer | qadeer <unknown> | 2010-08-27 05:07:49 +0000 |
| commit | 38681e1c890e9ef2cc90307e85c7d6df2578c725 (patch) | |
| tree | 2efaf778cdf8a3918f4790890495021b02154e8f /Source/Provers/Z3api/SafeContext.cs | |
| parent | c60b6a80965afe086396557c8090efac6bac94f3 (diff) | |
simplified the push-pop business
Diffstat (limited to 'Source/Provers/Z3api/SafeContext.cs')
| -rw-r--r-- | Source/Provers/Z3api/SafeContext.cs | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/Source/Provers/Z3api/SafeContext.cs b/Source/Provers/Z3api/SafeContext.cs index c6907639..67cff382 100644 --- a/Source/Provers/Z3api/SafeContext.cs +++ b/Source/Provers/Z3api/SafeContext.cs @@ -266,15 +266,6 @@ namespace Microsoft.Boogie.Z3 bound.Add(Unwrap(t));
}
Term termAst = z3.MkForall(weight, bound.ToArray(), unwrapPatterns.ToArray(), unwrapBody);
- /*
- Term termAst = z3.MkQuantifier(true,
- weight,
- unwrapPatterns.ToArray(),
- unwrapNoPatterns.ToArray(),
- z3Types.ToArray(),
- symbols.ToArray(),
- unwrapBody);
- */
return Wrap(termAst);
}
@@ -293,15 +284,6 @@ namespace Microsoft.Boogie.Z3 bound.Add(Unwrap(t));
}
Term termAst = z3.MkExists(weight, bound.ToArray(), unwrapPatterns.ToArray(), unwrapBody);
- /*
- Term termAst = z3.MkQuantifier(false,
- weight,
- unwrapPatterns.ToArray(),
- unwrapNoPatterns.ToArray(),
- z3Types.ToArray(),
- symbols.ToArray(),
- unwrapBody);
- */
return Wrap(termAst);
}
@@ -360,7 +342,6 @@ namespace Microsoft.Boogie.Z3 {
boogieErrors = new List<Z3ErrorModelAndLabels>();
LBool outcome = LBool.Undef;
- z3.Push();
while (boogieErrors.Count < this.config.Counterexamples)
{
Model z3Model;
@@ -382,7 +363,6 @@ namespace Microsoft.Boogie.Z3 else
break;
}
- z3.Pop();
if (boogieErrors.Count > 0)
return ProverInterface.Outcome.Invalid;
|