projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b8a5b45) | patch
Fix get-model when sort constructors are present (#7828)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 16 Dec 2021 21:07:55 +0000 (15:07 -0600)
committerGitHub <noreply@github.com>
Thu, 16 Dec 2021 21:07:55 +0000 (15:07 -0600)
commit0c21537af09a451e57cb6251ebba2c20c69cf612
tree0cefce3a09af94b29ae2a50186a547f833f7e317tree
parentb8a5b453e3a4f6d2ae15ac727358540b191c186ecommit | diff
Fix get-model when sort constructors are present (#7828)

Fixes a spurious error on kind benchmarks.

Note that we don't properly handle instantiated sort constructors currently, which I believe need to be handled as declared sorts when calling getModel.
src/smt/command.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/parser/get-model-sort-constructor.smt2 [new file with mode: 0644] blob