Skip to content

Commit 2227a3c

Browse files
Allow updating assertion_stats
This will allow us to call the register_assertion_ssas method twice to add the clauses of the goal disjunction.
1 parent 6f24efd commit 2227a3c

File tree

1 file changed

+5
-4
lines changed

1 file changed

+5
-4
lines changed

src/goto-symex/solver_hardness.cpp

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -77,11 +77,12 @@ void solver_hardnesst::register_assertion_ssas(
7777
const std::vector<goto_programt::const_targett> &pcs)
7878
{
7979
if(assertion_stats.empty())
80-
return;
80+
{
81+
assertion_stats.ssa_expression = expr2string(ssa_expression);
82+
assertion_stats.pcs = pcs;
83+
}
8184

82-
assertion_stats.sat_hardness = current_hardness;
83-
assertion_stats.ssa_expression = expr2string(ssa_expression);
84-
assertion_stats.pcs = pcs;
85+
assertion_stats.sat_hardness += current_hardness;
8586
current_ssa_key = {};
8687
current_hardness = {};
8788
}

0 commit comments

Comments
 (0)