Skip to content

Commit 34bcb1f

Browse files
author
Owen
committed
Move apply_condition from symex_assume_l2 to symex_assume
This is in preparation for putting try_filter_value_sets after it. As noted in the comment, it is important that it comes after rename.
1 parent 870bfd7 commit 34bcb1f

File tree

1 file changed

+4
-2
lines changed

1 file changed

+4
-2
lines changed

src/goto-symex/symex_main.cpp

+4-2
Original file line numberDiff line numberDiff line change
@@ -130,6 +130,10 @@ void goto_symext::symex_assume(statet &state, const exprt &cond)
130130
simplified_cond = state.rename(std::move(simplified_cond), ns).get();
131131
do_simplify(simplified_cond);
132132

133+
// apply_condition must come after rename because it might change the
134+
// constant propagator and the value-set and we read from those in rename
135+
state.apply_condition(simplified_cond, state, ns);
136+
133137
symex_assume_l2(state, simplified_cond);
134138
}
135139

@@ -160,8 +164,6 @@ void goto_symext::symex_assume_l2(statet &state, const exprt &cond)
160164
if(state.atomic_section_id!=0 &&
161165
state.guard.is_false())
162166
symex_atomic_end(state);
163-
164-
state.apply_condition(cond, state, ns);
165167
}
166168

167169
void goto_symext::rewrite_quantifiers(exprt &expr, statet &state)

0 commit comments

Comments
 (0)