projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: d02e1cb)
Fix (#1975)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 24 May 2018 19:24:44 +0000 (14:24 -0500)
committerGitHub <noreply@github.com>
Thu, 24 May 2018 19:24:44 +0000 (14:24 -0500)
src/theory/arith/nonlinear_extension.cpp patch | blob | history

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index be8f22222598385dc54cc7c1f804fa4e1d6c3499..a323ccddd59aaeebf6ad7e143d82db382b6b9d3d 100644 (file)
--- 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")