projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a05b134) | patch
Improve theory combination over real algebraic models (#8045)
authorGereon Kremer <gkremer@stanford.edu>
Thu, 3 Feb 2022 23:14:38 +0000 (15:14 -0800)
committerGitHub <noreply@github.com>
Thu, 3 Feb 2022 23:14:38 +0000 (23:14 +0000)
commit72bf82dade6b72cea4cb8bf86d03a7f6b875b3a9
treed866447d371116d52d37137711daf68999efd33btree
parenta05b134c4d7bc73d57f31a55330e543dc6c14f33commit | diff
Improve theory combination over real algebraic models (#8045)

Though we support real algebraic models now for theory combination, cvc5/cvc5-projects#451 uncovered the possibility to assert if an equality was in fact not equal during theory combination and the difference was real algebraic.
This PR fixes this issue by adding the proper check.
Fixes cvc5/cvc5-projects#451.
src/theory/arith/arith_evaluator.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/nl/proj-issue-451-ran-combination-1.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/proj-issue-451-ran-combination-2.smt2 [new file with mode: 0644] blob