From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 24 May 2018 19:24:44 +0000 (-0500)
Subject: Fix (#1975)
X-Git-Tag: cvc5-1.0.0~5013
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d12c7561624de9a2ae6cf10a7fa2bd9c97b2bc5e;p=cvc5.git

Fix (#1975)
---

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index be8f22222..a323ccddd 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -1735,7 +1735,7 @@ bool NonlinearExtension::simpleCheckModelMsum(const std::map<Node, Node>& msum,
           }
           else
           {
-            vc_set_lower = (signs[i] == setAbs);
+            vc_set_lower = (signs[i] != setAbs);
           }
           Trace("nl-ext-cms-debug")
               << "..." << vc << " set to " << (vc_set_lower ? "lower" : "upper")