projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: fe939c3) | patch
Ensure substitutions in nonlinear solver are properly typed (#8748)
authorGereon Kremer <gkremer@cs.stanford.edu>
Tue, 10 May 2022 21:23:20 +0000 (14:23 -0700)
committerGitHub <noreply@github.com>
Tue, 10 May 2022 21:23:20 +0000 (16:23 -0500)
commitb47d65698b514cfbe353182cab8e4261d74a020e
tree98352f009c67725d8a660234ad9c0caeb35bf4f5tree
parentfe939c31bd286675298990d7d1865d275d982679commit | diff
Ensure substitutions in nonlinear solver are properly typed (#8748)

We would apply substitutions between int and real terms, effectively hiding the intness of variables from the coverings solver.
Fixes #8744.
The example from #8744 times out after the fix, thus no regression.
src/theory/arith/nl/equality_substitution.cpp diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/nl/issue8744-int.smt2 [new file with mode: 0644] blob
test/regress/cli/regress0/nl/issue8744-real-cov.smt2 [new file with mode: 0644] blob
test/regress/cli/regress0/nl/issue8744-real.smt2 [new file with mode: 0644] blob