projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 3f09cf8) | patch
Consider APPLY_CONSTRUCTOR applied to values to be a value (#8284)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 11 Mar 2022 18:03:09 +0000 (12:03 -0600)
committerGitHub <noreply@github.com>
Fri, 11 Mar 2022 18:03:09 +0000 (18:03 +0000)
commit2b44509b23e23e6dfb29899ccb55ee39de287b07
tree336a4500d4ce2c48ad6e6f6d3b9ac7e52bd9e084tree
parent3f09cf86d8a0129c12afc6ee63445c2a714ce5f6commit | diff
Consider APPLY_CONSTRUCTOR applied to values to be a value (#8284)

Fixes cvc5/cvc5-projects#474.

Previously TheoryModel::isModelValue was incorrect for APPLY_CONSTRUCTOR.
src/theory/theory_model.cpp diff | blob | history
src/theory/theory_model_builder.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/datatypes/proj-issue474-app-cons-value.smt2 [new file with mode: 0644] blob