diff options
| author |  Pantazis Deligiannis <pdeligia@me.com> | 2013-07-09 02:23:50 +0100 |
|---|---|---|
| committer | Pantazis Deligiannis <pdeligia@me.com> | 2013-07-09 02:23:50 +0100 |
| commit | 33a6a3f30aab67619b93e7875f27f65c3b4ac316 (patch) | |
| tree | 2aba18d7ac28100db9953fe38061733d42d7ea0f /Source | |
| parent | a6ad13aab30cd2bdd9576c74bf58e7e2b9b855d5 (diff) | |
allows (reset) to be send only to the Z3 prover
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 20 |
1 files changed, 13 insertions, 7 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 4cb85435..c00545df 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -397,17 +397,23 @@ namespace Microsoft.Boogie.SMTLib public override void Reset()
{
- SendThisVC("(reset)");
- Process.Send(common.ToString());
+ if (options.Solver == SolverKind.Z3)
+ {
+ SendThisVC("(reset)");
+ Process.Send(common.ToString());
+ }
}
public override void FullReset()
{
- SendThisVC("(reset)");
- common.Clear();
- AxiomsAreSetup = false;
- ctx.Clear();
- DeclCollector.Reset();
+ if (options.Solver == SolverKind.Z3)
+ {
+ SendThisVC("(reset)");
+ common.Clear();
+ AxiomsAreSetup = false;
+ ctx.Clear();
+ DeclCollector.Reset();
+ }
}
private RPFP.Node SExprToCex(SExpr resp, ErrorHandler handler,
|