projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 425a28b) | patch
Disallow models with `--arrays-weak-equiv` (#8217)
authorAndres Noetzli <andres.noetzli@gmail.com>
Sun, 6 Mar 2022 16:02:26 +0000 (08:02 -0800)
committerGitHub <noreply@github.com>
Sun, 6 Mar 2022 16:02:26 +0000 (16:02 +0000)
commit3809343bf829523e425225cbf641a4fc62c713f7
tree2bd66e1489048bb06d046f08ba4a5a011a5cf907tree
parent425a28b996286c4eea66a96bad075fc342a9fed7commit | diff
Disallow models with `--arrays-weak-equiv` (#8217)

Fixes #2007. We currently do not support generating models when
`--arrays-weak-equiv` is enabled. This commit adds a corresponding
user-facing error message.
src/smt/set_defaults.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/arrays/issue8103-1-weak-equiv-models.smt2 [new file with mode: 0644] blob