diff options
4 files changed, 9 insertions, 2 deletions
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 0d85b8946..88da629a0 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -1088,7 +1088,8 @@ bool CegInstantiator::doAddInstantiation(std::vector<Node>& vars, bool CegInstantiator::isEligibleForInstantiation(Node n) const { - if (n.getKind() != INST_CONSTANT && n.getKind() != SKOLEM) + Kind nk = n.getKind(); + if (nk != INST_CONSTANT && nk != SKOLEM && nk != BOOLEAN_TERM_VARIABLE) { return true; } diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 81e5ca8c6..35d2553de 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -872,6 +872,7 @@ set(regress_0_tests regress0/quantifiers/issue4576.smt2 regress0/quantifiers/issue5645-dt-cm-spurious.smt2 regress0/quantifiers/issue5693-prenex.smt2 + regress0/quantifiers/issue6603-dt-bool-cegqi.smt2 regress0/quantifiers/lra-triv-gn.smt2 regress0/quantifiers/macro-back-subs-sat.smt2 regress0/quantifiers/macros-int-real.smt2 diff --git a/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2 b/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2 index 0d3f711bf..6ed3a1867 100644 --- a/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2 +++ b/test/regress/regress0/quantifiers/issue5645-dt-cm-spurious.smt2 @@ -1,5 +1,5 @@ (set-logic ALL) -(set-info :status sat) +(set-info :status unsat) (declare-datatypes ((Enum1 0)) (((None) (cons (data Bool))))) (assert (forall ((var_1 Enum1)) (data var_1))) (check-sat) diff --git a/test/regress/regress0/quantifiers/issue6603-dt-bool-cegqi.smt2 b/test/regress/regress0/quantifiers/issue6603-dt-bool-cegqi.smt2 new file mode 100644 index 000000000..fce67f4d0 --- /dev/null +++ b/test/regress/regress0/quantifiers/issue6603-dt-bool-cegqi.smt2 @@ -0,0 +1,5 @@ +(set-logic ALL) +(set-info :status unsat) +(declare-datatypes ((E 0)) (((c (a Bool))))) +(assert (forall ((v E)) (a v))) +(check-sat) |