From c8b95a25e4e458aad19ef3891e7a09d3032d2ac0 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 28 Dec 2017 19:24:35 -0800
Subject: Add unit tests for side conditions for inequality for CBQI BV.
 (#1455)

---
 src/theory/quantifiers/bv_inverter.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/theory/quantifiers/bv_inverter.cpp')

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index a970e3395..cdabaabb8 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -363,7 +363,7 @@ static Node getScBvUrem(bool pol,
                         Node t)
 {
   Assert(k == BITVECTOR_UREM_TOTAL);
-  Assert(pol == false || idx == 1);
+  Assert(litk != EQUAL || pol == false || idx == 1);
 
 
   NodeManager* nm = NodeManager::currentNM();
-- 
cgit v1.2.3