diff options
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/ProverInterface.cs | 16 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/TypeDeclCollector.cs | 5 |
2 files changed, 18 insertions, 3 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs index 08322ebb..014af458 100644 --- a/Source/Provers/SMTLib/ProverInterface.cs +++ b/Source/Provers/SMTLib/ProverInterface.cs @@ -78,14 +78,14 @@ namespace Microsoft.Boogie.SMTLib SetupProcess();
- if (CommandLineOptions.Clo.StratifiedInlining > 0)
+ if (CommandLineOptions.Clo.StratifiedInlining > 0 || CommandLineOptions.Clo.ContractInfer)
{
// Prepare for ApiChecker usage
if (options.LogFilename != null && currentLogFile == null)
{
currentLogFile = OpenOutputFile("");
}
- if (CommandLineOptions.Clo.ProcedureCopyBound > 0)
+ if (CommandLineOptions.Clo.ProcedureCopyBound > 0 || CommandLineOptions.Clo.ContractInfer)
{
SendThisVC("(set-option :produce-unsat-cores true)");
this.usingUnsatCore = true;
@@ -770,6 +770,14 @@ namespace Microsoft.Boogie.SMTLib SendThisVC(a);
}
+ public override void DefineMacro(Function fun, VCExpr vc) {
+ DeclCollector.AddFunction(fun);
+ string name = Namer.GetName(fun, fun.Name);
+ string a = "(define-fun " + name + "() Bool " + VCExpr2String(vc, 1) + ")";
+ AssertAxioms();
+ SendThisVC(a);
+ }
+
public override void AssertAxioms()
{
FlushAxioms();
@@ -805,7 +813,9 @@ namespace Microsoft.Boogie.SMTLib nameCounter++;
nameToAssumption.Add(name, i);
- SendThisVC(string.Format("(assert (! {0} :named {1}))", VCExpr2String(vc, 1), name));
+ string vcString = VCExpr2String(vc, 1);
+ AssertAxioms();
+ SendThisVC(string.Format("(assert (! {0} :named {1}))", vcString, name));
i++;
}
Check();
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index 05a6caf3..a4bdee51 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -164,6 +164,11 @@ void ObjectInvariant() return TypeToString(t);
}
+ public void AddFunction(Function func) {
+ if (KnownFunctions.Contains(func))
+ return;
+ KnownFunctions.Add(func);
+ }
public override bool Visit(VCExprNAry node, bool arg) {
Contract.Requires(node != null);
|