From 8a389f98c20a9e308b8a74b0dd5fb6d79fe5a9b8 Mon Sep 17 00:00:00 2001
From: polgreen <elizabeth.polgreen@cs.ox.ac.uk>
Date: Wed, 22 Nov 2017 14:13:57 +0000
Subject: [PATCH] Hook for cegis to freeze program variables

---
 src/cbmc/bmc.cpp | 13 +++++++++++++
 src/cbmc/bmc.h   |  2 ++
 2 files changed, 15 insertions(+)

diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 49bb2941a8b..9b8e2e4500c 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -45,6 +45,17 @@ void bmct::do_unwind_module()
   // this is a hook for hw-cbmc
 }
 
+/// Hook used by CEGIS to selectively freeze variables
+/// in the SAT solver after the SSA formula is added to the solver.
+/// Freezing variables is necessary to make use of incremental
+/// solving with MiniSat SimpSolver.
+/// Potentially a useful hook for other applications using
+/// incremental solving.
+void bmct::freeze_program_variables()
+{
+  // this is a hook for cegis
+}
+
 void bmct::error_trace()
 {
   status() << "Building error trace" << eom;
@@ -131,6 +142,8 @@ void bmct::do_conversion()
     forall_expr_list(it, bmc_constraints)
       prop_conv.set_to_true(*it);
   }
+  // hook for cegis to freeze synthesis program vars
+  freeze_program_variables();
 }
 
 decision_proceduret::resultt
diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h
index 7903482913d..c81ee66e74b 100644
--- a/src/cbmc/bmc.h
+++ b/src/cbmc/bmc.h
@@ -92,6 +92,8 @@ class bmct:public safety_checkert
   virtual void do_unwind_module();
   void do_conversion();
 
+  virtual void freeze_program_variables();
+
   virtual void show_vcc();
   virtual void show_vcc_plain(std::ostream &out);
   virtual void show_vcc_json(std::ostream &out);