From: Tim King <taking@cs.nyu.edu>
Date: Mon, 19 Nov 2012 17:16:16 +0000 (+0000)
Subject: Changed the splitting-on-demand lemmas of arithmetic to no longer contain the equalit... 
X-Git-Tag: cvc5-1.0.0~7574
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1f80df98e2766a0202741d9e924bf842ba2225b5;p=cvc5.git

Changed the splitting-on-demand lemmas of arithmetic to no longer contain the equality being split on. Instead of issuing 'x != y implies (x < y or x > y)', the lemma is now '(x <= y or x >= y)'. This resolves bug 450.
---

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 792d4b16c..392d04f6c 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -590,10 +590,10 @@ Node ConstraintValue::split(){
   TNode lhs = eqNode[0];
   TNode rhs = eqNode[1];
 
-  Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs;
-  Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs;
+  Node leqNode = NodeBuilder<2>(kind::LEQ) << lhs << rhs;
+  Node geqNode = NodeBuilder<2>(kind::GEQ) << lhs << rhs;
 
-  Node lemma = NodeBuilder<3>(OR) << eqNode << ltNode << gtNode;
+  Node lemma = NodeBuilder<3>(OR) << leqNode << geqNode;
 
 
   eq->d_database->pushSplitWatch(eq);