projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 55be526) | patch
Add two regressions related to RAN models (#8142)
authorGereon Kremer <gkremer@cs.stanford.edu>
Wed, 23 Feb 2022 23:06:31 +0000 (00:06 +0100)
committerGitHub <noreply@github.com>
Wed, 23 Feb 2022 23:06:31 +0000 (23:06 +0000)
commit5c902c8c0bc8e7d8aaa543b048345495c7ec48cd
tree46652bfb3bc7920c92cbe2ed6c5523edb2b5043etree
parent55be526dfb5bafa3d27cc1dc5de9ee6d668eba94commit | diff
Add two regressions related to RAN models (#8142)

This PR adds regressions for two issues that relate to the previously incomplete handling of real algebraic models.
The issue has been resolved by properly integrating real algebraic numbers as model values and in the rewriter.
Fixes #6547. Fixes #6619.
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/nl/issue6547-ran-model.smt2 [new file with mode: 0644] blob
test/regress/regress0/nl/issue6619-ran-model.smt2 [new file with mode: 0644] blob