Skip to content

Commit

Permalink
Move asserts inside conditional (#367)
Browse files Browse the repository at this point in the history
These checks only need to be performed again if there actually is a change to the term.
  • Loading branch information
CyanoKobalamyne authored Jan 24, 2025
1 parent 52826f6 commit 97ab021
Showing 1 changed file with 3 additions and 4 deletions.
7 changes: 3 additions & 4 deletions engines/ic3base.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -358,11 +358,10 @@ bool IC3Base::reaches_bad(IC3Formula & out)
if (options_.ic3_pregen_) {
// try to generalize if predecessor generalization enabled
predecessor_generalization_and_fix(frames_.size(), bad_, out);
assert(out.term);
assert(out.children.size());
assert(ic3formula_check_valid(out));
}

assert(out.term);
assert(out.children.size());
assert(ic3formula_check_valid(out));
}

pop_solver_context();
Expand Down

0 comments on commit 97ab021

Please sign in to comment.