From 2d0d527fe1af9349e172b181dfeacb50fa75c6fd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Mar 2020 16:56:49 -0700 Subject: [PATCH] preserve model order to avoid clobbering regression tests Signed-off-by: Nikolaj Bjorner --- src/muz/spacer/spacer_unsat_core_learner.cpp | 1 - src/tactic/model_converter.cpp | 4 ++-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/muz/spacer/spacer_unsat_core_learner.cpp b/src/muz/spacer/spacer_unsat_core_learner.cpp index 730ef1629..162b8c614 100644 --- a/src/muz/spacer/spacer_unsat_core_learner.cpp +++ b/src/muz/spacer/spacer_unsat_core_learner.cpp @@ -15,7 +15,6 @@ Revision History: --*/ -#include #include "ast/for_each_expr.h" #include "ast/proofs/proof_utils.h" diff --git a/src/tactic/model_converter.cpp b/src/tactic/model_converter.cpp index 41b9a08ea..127c7ef10 100644 --- a/src/tactic/model_converter.cpp +++ b/src/tactic/model_converter.cpp @@ -131,11 +131,11 @@ public: m = m_model; return; } - for (unsigned i = m_model->get_num_constants(); i-- > 0; ) { + for (unsigned i = 0; i < m_model->get_num_constants(); ++i) { func_decl* f = m_model->get_constant(i); m->register_decl(f, m_model->get_const_interp(f)); } - for (unsigned i = m_model->get_num_functions(); i-- > 0; ) { + for (unsigned i = 0; i < m_model->get_num_functions(); ++i) { func_decl* f = m_model->get_function(i); m->register_decl(f, m_model->get_func_interp(f)->copy()); }