projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3243a93) | patch
Weaken assertion in CEGQI (#7548)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 1 Nov 2021 23:04:16 +0000 (18:04 -0500)
committerGitHub <noreply@github.com>
Mon, 1 Nov 2021 23:04:16 +0000 (23:04 +0000)
commitb57e39bab5e27b883f01818a401404736c6ce02e
tree333435d9d46425093958961e8320b4c24052e8c1tree
parent3243a93ed9ae38f7789f857b0f8f9cc160139620commit | diff
Weaken assertion in CEGQI (#7548)

The assertion can be violated in mixed Int/Real arithmetic. The instantiator utility nevertheless safe guards Int vs Real subtyping.

Fixes #7537.
src/theory/quantifiers/cegqi/ceg_instantiator.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/quantifiers/issue7537-cegqi-comp-types.smt2 [new file with mode: 0644] blob