From f57f6138b4a9d9cb9c6096ea10072132bc3677b5 Mon Sep 17 00:00:00 2001 From: Lev Date: Wed, 26 Dec 2018 20:39:33 -0800 Subject: [PATCH] fix a bug in order lemma Signed-off-by: Lev --- src/util/lp/nla_solver.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 709985ef3..32e4fdaea 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -1567,10 +1567,10 @@ struct solver::imp { SASSERT(akey.size() == bkey.size()); for (unsigned i = 0; i < akey.size(); i++) { if (i != strict) { - negate_abs_a_le_abs_b(a[i], b[i]); + negate_abs_a_le_abs_b(akey[i].second, bkey[i].second); } else { mk_ineq(b[i], llc::EQ); - negate_abs_a_lt_abs_b(a[i], b[i]); + negate_abs_a_lt_abs_b(akey[i].second, bkey[i].second); } } assert_abs_val_a_le_abs_var_b(a, b, true);