From 6b995c4077b959f02ebae5f0fdb31b69ab30d284 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 2 Apr 2015 02:56:40 -0700 Subject: [PATCH] disable wrong fix for simplification Signed-off-by: Nikolaj Bjorner --- src/smt/asserted_formulas.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index faf5ce0ef..1acfcdf57 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -603,7 +603,7 @@ void asserted_formulas::propagate_values() { proof_ref_vector new_prs1(m_manager); expr_ref_vector new_exprs2(m_manager); proof_ref_vector new_prs2(m_manager); - unsigned i = 0; + unsigned i = m_asserted_qhead; unsigned sz = m_asserted_formulas.size(); for (; i < sz; i++) { expr * n = m_asserted_formulas.get(i);