From 90daf35ed33e5da9d744e24bf00f7d29b82c4859 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 23 May 2022 16:11:07 -0500 Subject: [PATCH] Remove spurious assertion in isLegalElimination (#8812) Fixes #8805. The isLegalElimination method correctly catches Int -> Real as an illegal elimination. --- src/theory/theory.cpp | 2 -- test/regress/cli/CMakeLists.txt | 1 + .../cli/regress0/arith/issue8805-mixed-var-elim.smt2 | 6 ++++++ 3 files changed, 7 insertions(+), 2 deletions(-) create mode 100644 test/regress/cli/regress0/arith/issue8805-mixed-var-elim.smt2 diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index d5df7084a..9ba9ad028 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -322,8 +322,6 @@ bool Theory::isLegalElimination(TNode x, TNode val) } if (val.getType() != x.getType()) { - Assert(false) << "isLegalElimination for disequal typed terms " << x - << " -> " << val; return false; } if (!options().smt.produceModels || options().smt.modelVarElimUneval) diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt index 5156d97df..a9d2f4f6e 100644 --- a/test/regress/cli/CMakeLists.txt +++ b/test/regress/cli/CMakeLists.txt @@ -67,6 +67,7 @@ set(regress_0_tests regress0/arith/issue5761-ppr.smt2 regress0/arith/issue8097-iid.smt2 regress0/arith/issue8159-rewrite-intreal.smt2 + regress0/arith/issue8805-mixed-var-elim.smt2 regress0/arith/ite-lift.smt2 regress0/arith/leq.01.smtv1.smt2 regress0/arith/miplib.cvc.smt2 diff --git a/test/regress/cli/regress0/arith/issue8805-mixed-var-elim.smt2 b/test/regress/cli/regress0/arith/issue8805-mixed-var-elim.smt2 new file mode 100644 index 000000000..5fa5684b5 --- /dev/null +++ b/test/regress/cli/regress0/arith/issue8805-mixed-var-elim.smt2 @@ -0,0 +1,6 @@ +(set-logic ALL) +(set-info :status sat) +(declare-const a Real) +(declare-const b Int) +(assert (= (to_real b) (* a a))) +(check-sat) -- 2.30.2