projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b62070d) | patch
Allow for multiple (equal) base model values (#8467)
authorGereon Kremer <gkremer@cs.stanford.edu>
Wed, 30 Mar 2022 23:44:49 +0000 (01:44 +0200)
committerGitHub <noreply@github.com>
Wed, 30 Mar 2022 23:44:49 +0000 (23:44 +0000)
commit019be6360c21a4899debbcc4e2615be2fbe08974
tree08c8c1946cf93f7908ae134b32d338550a3b958ftree
parentb62070dc7a819b092a27f416349d091ac60bb6e4commit | diff
Allow for multiple (equal) base model values (#8467)

This PR weakens an assertion about multiple model values in the same equivalence class. We now accept multiple base model values in the same equivalence class, as long as they compare equal. This allows to gracefully handle cases where real algebraic numbers fail to realize that they are rational.
Fixes #8414.
src/theory/theory_model_builder.cpp diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress0/nl/issue8414-ran-rational.smt2 [new file with mode: 0644] blob