diff options
| author |  MichalMoskal <unknown> | 2011-02-23 00:49:51 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-02-23 00:49:51 +0000 |
| commit | 5f85e8afb614999c43df1d4cff399a4875125270 (patch) | |
| tree | 980f049e483da07ba1f620f4263ca0ab0ea4b202 /Source/Provers | |
| parent | 400d0e997dda5e56ddefff919d922419bd3775ba (diff) | |
Provide dummy implementation of FlushAxiomsToTheoremProver()
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index a034c37d..ee9e5df2 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -169,6 +169,12 @@ namespace Microsoft.Boogie.SMTLib }
}
+ public override int FlushAxiomsToTheoremProver()
+ {
+ // we feed the axioms when begincheck is called.
+ return 0;
+ }
+
private void FlushAxioms()
{
TypeDecls.Iter(SendCommon);
|