From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 3 Jan 2018 02:17:06 +0000 (-0800)
Subject: Simplify side condition for SGE over UREM (index = 1) for CBQI BV. (#1463)
X-Git-Tag: cvc5-1.0.0~5393
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=06ca7e3709fefbbec5d20f9c99e4a630a391dc28;p=cvc5.git

Simplify side condition for SGE over UREM (index = 1) for CBQI BV. (#1463)
---

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 8068b563e..67ce8d217 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -517,20 +517,16 @@ static Node getScBvUrem(bool pol,
         /* s % x < t
          * with side condition:
          * (and
-         *   (=> (= s z) (bvsle t z))
-         *   (=> (bvsgt s z) (bvsge s t))
+         *   (=> (bvsge s z) (bvsge s t))
          *   (=> (and (bvslt s z) (bvsge t z)) (bvugt (bvsub s t) t)))
          * where z = 0 with getSize(z) = w  */
         Node i1 = nm->mkNode(IMPLIES,
-            s.eqNode(z), nm->mkNode(BITVECTOR_SLE, t, z));
+            nm->mkNode(BITVECTOR_SGE, s, z), nm->mkNode(BITVECTOR_SGE, s, t));
         Node i2 = nm->mkNode(IMPLIES,
-            nm->mkNode(BITVECTOR_SLT, s, z), nm->mkNode(BITVECTOR_SGE, s, t));
-        Node i3 = nm->mkNode(IMPLIES,
             nm->mkNode(AND,
               nm->mkNode(BITVECTOR_SLT, s, z), nm->mkNode(BITVECTOR_SGE, t, z)),
             nm->mkNode(BITVECTOR_UGT, nm->mkNode(BITVECTOR_SUB, s, t), t));
-        scl = nm->mkNode(AND, i1, i2, i3);
-        return Node::null();
+        scl = nm->mkNode(AND, i1, i2);
       }
     }
   }