mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

fix reference counting bug in qe

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-02-06 09:40:16 -08:00
parent 8354c2dfb1
commit 0fd1c00053
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/muz_qe/qe_arith_plugin.cpp
View file

@ -524,7 +524,8 @@ namespace qe {
expr_ref as_bt_le_0(result, m), tmp2(m), tmp3(m), tmp4(m);
// a*s + b*t + (a-1)(b-1) <= 0
mk_le(m_arith.mk_add(as_bt, slack), result1);
tmp2 = m_arith.mk_add(as_bt, slack);
mk_le(tmp2, result1);
rational a1 = a, b1 = b;
if (abs_a < abs_b) {