projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 7b40844) | patch
Use debug-check-model to enable internal debugging in check-model (#4480)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 20 May 2020 05:05:58 +0000 (00:05 -0500)
committerGitHub <noreply@github.com>
Wed, 20 May 2020 05:05:58 +0000 (00:05 -0500)
commit927066eaecfc2c6f00aa1aca695b68e70164aae3
tree7456a1ec973f80aa806b66a8a2c6b6a8dfc3b4batree
parent7b4084440bd9dde894ff46c2ba0197fed41d91d1commit | diff
Use debug-check-model to enable internal debugging in check-model (#4480)

Notice this also updates our regression script to use --debug-check-model, preserving previous behavior.

Fixes #4461, fixes #4470, fixes #4471, fixes #4475, fixes #4448, fixes #4466, fixes #4460, fixes #4458, fixes #4455, fixes #4456, fixes #4386, fixes #4385, fixes #4478, fixes #4474.
src/options/smt_options.toml diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
src/theory/theory_model_builder.cpp diff | blob | history
test/regress/run_regression.py diff | blob | history