From a51aed01331839250c9a8aa6466ab204b7a59a80 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 24 Feb 2015 21:26:25 +0000 Subject: [PATCH] Fixed bug in constant propagation Signed-off-by: Christoph M. Wintersteiger --- 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 1acfcdf57..faf5ce0ef 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 = m_asserted_qhead; + unsigned i = 0; unsigned sz = m_asserted_formulas.size(); for (; i < sz; i++) { expr * n = m_asserted_formulas.get(i);