Fix assertion failure in sort inference for Boolean equalities (#3993)

Fixes #3990.

diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp
index 33a50960cec606d087471d32086b12782b77adcf..07d156c98aaf64bbbcde2a061dc96119d9845080 100644 (file)
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -663,7 +663,10 @@ Node SortInference::simplifyNode(
           Assert(d_op_arg_types.find(op) != d_op_arg_types.end());
           tnnc = getOrCreateTypeForId( d_op_arg_types[op][i], n[i].getType() );
           Assert(!tnnc.isNull());
-        }else if( n.getKind()==kind::EQUAL && i==0 ){
+        }
+        else if (n.getKind() == kind::EQUAL && !n[0].getType().isBoolean()
+                 && i == 0)
+        {
           Assert(d_equality_types.find(n) != d_equality_types.end());
           tnnc = getOrCreateTypeForId( d_equality_types[n], n[0].getType() );
           Assert(!tnnc.isNull());

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 35d5c5bd551ced37f3ed44d9ef67d2325c8911d3..6579894e9489afafd91f5a8cd4354ba137b3e5e8 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1299,6 +1299,7 @@ set(regress_1_tests
   regress1/hole6.cvc
   regress1/ite5.smt2
   regress1/issue3970-nl-ext-purify.smt2
+  regress1/issue3990-sort-inference.smt2
   regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2
   regress1/lemmas/pursuit-safety-8.smtv1.smt2
   regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2

diff --git a/test/regress/regress1/issue3990-sort-inference.smt2 b/test/regress/regress1/issue3990-sort-inference.smt2
new file mode 100644 (file)
index 0000000..f048718
--- /dev/null
+++ b/test/regress/regress1/issue3990-sort-inference.smt2
@@ -0,0 +1,35 @@
+(set-logic ABV)
+(set-option :sort-inference true)
+(set-info :status unsat)
+(declare-const v0 Bool)
+(declare-const v1 Bool)
+(declare-const v2 Bool)
+(declare-const v3 Bool)
+(declare-const v4 Bool)
+(declare-const v5 Bool)
+(declare-const v6 Bool)
+(declare-const v7 Bool)
+(declare-const v8 Bool)
+(declare-const v9 Bool)
+(declare-const v10 Bool)
+(declare-const v11 Bool)
+(declare-const v12 Bool)
+(declare-const v13 Bool)
+(assert (= v13 v3 v10 v5 v7 v8))
+(declare-const bv_10-0 (_ BitVec 10))
+(declare-const v14 Bool)
+(assert v8)
+(declare-const v15 Bool)
+(declare-const v16 Bool)
+(declare-const bv_25-0 (_ BitVec 25))
+(declare-const bv_4-0 (_ BitVec 4))
+(declare-const v17 Bool)
+(declare-const v18 Bool)
+(assert (not (not v13)))
+(assert (and v9 v11 v5 v4 v11 (and (= v13 v3 v10 v5 v7 v8) v9) v4 v4 v9 (xor v8 v6 (not v13) (xor (= v13 v3 v10 v5 v7 v8) v10) v12) (distinct v15 v13 v13 v2 v15 v7)))
+(declare-const v19 Bool)
+(assert (= v13 v3 v10 v5 v7 v8))
+(assert (forall ((q0 (_ BitVec 4)) (q1 (_ BitVec 4)) (q2 (_ BitVec 25)) (q3 (_ BitVec 4))) (=> (distinct bv_25-0 (bvsmod bv_25-0 bv_25-0) bv_25-0) (bvsle bv_4-0 bv_4-0))))
+(declare-const bv_13-0 (_ BitVec 13))
+(assert (exists ((q4 (_ BitVec 1))) v7))
+(check-sat)