Skip to content

Commit 856bcd4

Browse files
committed
convert_assertions: do not attempt to re-convert assumptions
convert_assumptions already took care of the conversion, and we can just use the resulting literal to force that to true.
1 parent 5fe1967 commit 856bcd4

File tree

1 file changed

+4
-4
lines changed

1 file changed

+4
-4
lines changed

src/goto-symex/symex_target_equation.cpp

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -444,6 +444,7 @@ void symex_target_equationt::convert_assumptions(
444444
with_solver_hardness(
445445
decision_procedure, hardness_register_ssa(step_index, step));
446446
}
447+
step.converted = true;
447448
}
448449
++step_index;
449450
}
@@ -532,10 +533,8 @@ void symex_target_equationt::convert_assertions(
532533
}
533534
else if(step.is_assume())
534535
{
535-
decision_procedure.set_to_true(step.cond_expr);
536-
537-
with_solver_hardness(
538-
decision_procedure, hardness_register_ssa(step_index, step));
536+
PRECONDITION(step.converted);
537+
decision_procedure.set_to_true(step.cond_handle);
539538
}
540539
++step_index;
541540
}
@@ -585,6 +584,7 @@ void symex_target_equationt::convert_assertions(
585584
}
586585
else if(step.is_assume())
587586
{
587+
PRECONDITION(step.converted);
588588
// the assumptions have been converted before
589589
// avoid deep nesting of ID_and expressions
590590
if(assumption.id()==ID_and)

0 commit comments

Comments
 (0)