mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 21:57:00 +00:00
Code Activity

Fixed bug in constant propagation

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-02-24 21:26:25 +00:00
parent f0967c0572
commit a51aed0133
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/asserted_formulas.cpp
View file

@ -603,7 +603,7 @@ void asserted_formulas::propagate_values() {
proof_ref_vector new_prs1(m_manager); proof_ref_vector new_prs1(m_manager);
expr_ref_vector new_exprs2(m_manager); expr_ref_vector new_exprs2(m_manager);
proof_ref_vector new_prs2(m_manager); proof_ref_vector new_prs2(m_manager);
unsigned i = m_asserted_qhead; unsigned i = 0;
unsigned sz = m_asserted_formulas.size(); unsigned sz = m_asserted_formulas.size();
for (; i < sz; i++) { for (; i < sz; i++) {
expr * n = m_asserted_formulas.get(i); expr * n = m_asserted_formulas.get(i);