Getting fixed point backend to work with Corral.

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;

     }