Merge pull request #8122 from diffblue/push_literal_exprt

simplify prop_conv_solvert::push
diffblue · Dec 19, 2023 · 92e3c0f · 92e3c0f
2 parents 3a1272a + 00e5975
commit 92e3c0f
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 3 deletions.
diff --git a/src/goto-checker/goto_symex_fault_localizer.cpp b/src/goto-checker/goto_symex_fault_localizer.cpp
@@ -95,7 +95,7 @@ bool goto_symex_fault_localizert::check(
   }
 
   // lock the failed assertion
-  assumptions.push_back(solver.handle(not_exprt(failed_step.cond_handle)));
+  assumptions.push_back(not_exprt(failed_step.cond_handle));
 
   solver.push(assumptions);
 

diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp
@@ -463,7 +463,7 @@ prop_conv_solvert::dec_solve(const exprt &assumption)
   if(assumption.is_nil())
     push();
   else
-    push({literal_exprt(convert(assumption))});
+    push({assumption});
 
   auto prop_result = prop.prop_solve(assumption_stack);
 
@@ -539,7 +539,12 @@ void prop_conv_solvert::push(const std::vector<exprt> &assumptions)
   // We push the given assumptions as a single context onto the stack.
   assumption_stack.reserve(assumption_stack.size() + assumptions.size());
   for(const auto &assumption : assumptions)
-    assumption_stack.push_back(to_literal_expr(assumption).get_literal());
+  {
+    auto literal = convert(assumption);
+    if(!literal.is_constant())
+      set_frozen(literal);
+    assumption_stack.push_back(literal);
+  }
   context_size_stack.push_back(assumptions.size());
 }