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();