diff --git a/src/muz/spacer/spacer_proof_utils.cpp b/src/muz/spacer/spacer_proof_utils.cpp index 4a64f3d08..082cc4b5d 100644 --- a/src/muz/spacer/spacer_proof_utils.cpp +++ b/src/muz/spacer/spacer_proof_utils.cpp @@ -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);