summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/ProverInterface.cs
diff options
context:
space:
mode:
Diffstat (limited to 'Source/Provers/SMTLib/ProverInterface.cs')
-rw-r--r--Source/Provers/SMTLib/ProverInterface.cs2
1 files changed, 2 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/ProverInterface.cs b/Source/Provers/SMTLib/ProverInterface.cs
index f2628130..be98eb5b 100644
--- a/Source/Provers/SMTLib/ProverInterface.cs
+++ b/Source/Provers/SMTLib/ProverInterface.cs
@@ -560,6 +560,7 @@ namespace Microsoft.Boogie.SMTLib
currentLogFile.Write(common.ToString());
}
+ SendThisVC("(fixedpoint-push)");
foreach (var node in rpfp.nodes)
{
DeclCollector.RegisterRelation((node.Name as VCExprBoogieFunctionOp).Func);
@@ -649,6 +650,7 @@ namespace Microsoft.Boogie.SMTLib
}
#endif
}
+ SendThisVC("(fixedpoint-pop)");
return result;
}