Remove spurious assertion in isLegalElimination (#8812)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 23 May 2022 21:11:07 +0000 (16:11 -0500)
committerGitHub <noreply@github.com>
Mon, 23 May 2022 21:11:07 +0000 (21:11 +0000)
commit90daf35ed33e5da9d744e24bf00f7d29b82c4859
treee24cc45893bab691c758cb8389e4793269e777b9
parent4338d9d49a41022d34cd4cbabf17a66fdf39efae
Remove spurious assertion in isLegalElimination (#8812)

Fixes #8805.

The isLegalElimination method correctly catches Int -> Real as an illegal elimination.
src/theory/theory.cpp
test/regress/cli/CMakeLists.txt
test/regress/cli/regress0/arith/issue8805-mixed-var-elim.smt2 [new file with mode: 0644]