mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
sort hypotheses
This commit is contained in:
parent
c5fb1c1223
commit
0534b72c4d
|
@ -427,6 +427,8 @@ proof* hypothesis_reducer::mk_lemma_core(proof* premise, expr *fact) {
|
|||
return premise;
|
||||
}
|
||||
|
||||
// add some stability
|
||||
std::stable_sort(active_hyps->begin(), active_hyps->end(), ast_lt_proc());
|
||||
// otherwise, build a disjunction of the negated active hypotheses
|
||||
// and add a lemma proof step
|
||||
expr_ref_buffer args(m);
|
||||
|
|
Loading…
Reference in a new issue