From 9ab7a86c46ebeab243a768a6240c2ecfb0b7464d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 14 Apr 2022 08:16:49 -0500 Subject: [PATCH] Fix spurious assertion involving subtypes (#8611) Fixes #8609. --- src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 2 +- test/regress/cli/CMakeLists.txt | 1 + .../cli/regress0/quantifiers/issue8609-subtype-assert.smt2 | 4 ++++ 3 files changed, 6 insertions(+), 1 deletion(-) create mode 100644 test/regress/cli/regress0/quantifiers/issue8609-subtype-assert.smt2 diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index f09faf22f..dbb6c6acc 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -1234,7 +1234,7 @@ Node CegInstantiator::applySubstitution( TypeNode tn, Node n, std::vector< Node Node v = msum_term[it->first]; if (!v.isNull()) { - Assert(v.getType() == type); + Assert(v.getType().isComparableTo(type)); c = nm->mkNode(MULT, c, v); } children.push_back( c ); diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 99ca3b969..dbdd97c83 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -1061,6 +1061,7 @@ set(regress_0_tests regress0/quantifiers/issue8159-3-qext-nterm.smt2 regress0/quantifiers/issue8227-subs-shadow.smt2 regress0/quantifiers/issue8466-syqi-bool.smt2 + regress0/quantifiers/issue8609-subtype-assert.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/cli/regress0/quantifiers/issue8609-subtype-assert.smt2 b/test/regress/cli/regress0/quantifiers/issue8609-subtype-assert.smt2 new file mode 100644 index 000000000..a85afb034 --- /dev/null +++ b/test/regress/cli/regress0/quantifiers/issue8609-subtype-assert.smt2 @@ -0,0 +1,4 @@ +(set-logic ALL) +(set-info :status unsat) +(assert (forall ((r Int) (r9 Int)) (= 1.0 (/ (to_real r) (+ 0.5 (to_real r9)))))) +(check-sat) -- 2.30.2