From b33f223d4d0e8b2e72a9779dd38a5aa836bfb7f4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@hm.edu>
Date: Fri, 22 Sep 2023 12:05:52 +0200
Subject: [PATCH] Freeze property literal for incremental analysis

MiniSAT melts assumed literals that were not explicitly frozen before. Therefore
checking two equal properties could result in the property literal being
eliminated if the solver was run with different assumptions between the two
checks.
---
 src/ebmc/ebmc_base.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/ebmc/ebmc_base.cpp b/src/ebmc/ebmc_base.cpp
index 3bfd5674a..baa7610f7 100644
--- a/src/ebmc/ebmc_base.cpp
+++ b/src/ebmc/ebmc_base.cpp
@@ -134,7 +134,8 @@ int ebmc_baset::finish_bmc(prop_conv_solvert &solver) {
       disjuncts.push_back(literal_exprt(!l));
 
     auto converted_or = solver.convert(disjunction(disjuncts));
-    solver.push({literal_exprt{converted_or}});
+    solver.push({literal_exprt(converted_or)});
+    solver.set_frozen(converted_or);
 
     decision_proceduret::resultt dec_result=
       solver.dec_solve();