diff options
| author |  MichalMoskal <unknown> | 2011-02-21 21:53:15 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-02-21 21:53:15 +0000 |
| commit | 99ad9968961ed7d9fa29a9ca1fa1f0637e103e3c (patch) | |
| tree | 962ad89ee0eb69afde03aab16f6811c432e02621 /Source/Provers | |
| parent | 86e9b76cd4b6932cdd20c0d5aaf298c849114d72 (diff) | |
Per SMT standard push requires an argument
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index e48446d9..35027e0e 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -212,7 +212,7 @@ namespace Microsoft.Boogie.SMTLib string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
FlushAxioms();
- SendThisVC("(push)");
+ SendThisVC("(push 1)");
SendThisVC("(set-info :boogie-vc-id " + SMTLibNamer.QuoteId(descriptiveName) + ")");
SendThisVC(vcString);
FlushLogFile();
|