From ee2aed38e88ced1afbf09c867487fff190357195 Mon Sep 17 00:00:00 2001 From: Lev Date: Fri, 28 Sep 2018 10:52:47 -0700 Subject: [PATCH] switch pos ( sign) when creating literals for EQ and NE Signed-off-by: Lev --- src/smt/theory_lra.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 0648c4a66..19dfa6888 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2085,8 +2085,8 @@ public: case lp::LT: is_lower = true; pos = true; break; case lp::GE: is_lower = true; pos = false; break; case lp::GT: is_lower = false; pos = true; break; - case lp::EQ: is_eq = true; pos = true; break; - case lp::NE: is_eq = true; pos = false; break; + case lp::EQ: is_eq = true; pos = false; break; + case lp::NE: is_eq = true; pos = true; break; default: UNREACHABLE(); } TRACE("arith", tout << "is_lower: " << is_lower << " pos " << pos << "\n";);