From 0534b72c4dd53949c6f10c12b08a1448b35340dd Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Thu, 7 Jun 2018 09:54:44 -0700 Subject: [PATCH] sort hypotheses --- src/muz/spacer/spacer_proof_utils.cpp | 2 ++ 1 file changed, 2 insertions(+) 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);