From c79af53f668745317ed92fa223035d285678c987 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 10 Mar 2020 11:58:06 -0500 Subject: [PATCH] Fix assertion failure in sort inference for Boolean equalities (#3993) Fixes #3990. --- src/theory/sort_inference.cpp | 5 ++- test/regress/CMakeLists.txt | 1 + .../regress1/issue3990-sort-inference.smt2 | 35 +++++++++++++++++++ 3 files changed, 40 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress1/issue3990-sort-inference.smt2 diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp index 33a50960c..07d156c98 100644 --- 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 35d5c5bd5..6579894e9 100644 --- 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 index 000000000..f048718a8 --- /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) -- 2.30.2