mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

fix #1376

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-27 08:39:20 -08:00
parent 4520fafa8c
commit bfe6260c58
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/theory_seq.cpp
View file

@ -2400,6 +2400,7 @@ bool theory_seq::add_stoi_axiom(expr* e) {
nums[i] = m_autil.mk_mul(coeff, nums[i].get()); nums[i] = m_autil.mk_mul(coeff, nums[i].get());
} }
num = m_autil.mk_add(nums.size(), nums.c_ptr()); num = m_autil.mk_add(nums.size(), nums.c_ptr());
ctx.get_rewriter()(num);
lits.push_back(mk_eq(e, num, false)); lits.push_back(mk_eq(e, num, false));
++m_stats.m_add_axiom; ++m_stats.m_add_axiom;
m_new_propagation = true; m_new_propagation = true;