projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 940a252) | patch
Fix assertion related to assignability in the model. (#3843)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sat, 29 Feb 2020 04:30:40 +0000 (22:30 -0600)
committerGitHub <noreply@github.com>
Sat, 29 Feb 2020 04:30:40 +0000 (20:30 -0800)
commit4ac14c09322f234ba2a201e0d281664338fd9ee0
tree842c67e61698fac5a82125c65ad77b049bc9349ftree
parent940a25255469bbeea95df14ef25036e6c0565c3ecommit | diff
Fix assertion related to assignability in the model. (#3843)

Fixes #3813.

It appears that an assertion was hardcoded to check whether a term was a variable or APPLY_UF application whereas this check should use isAssignable. This avoids an assertion failure on the given benchmark.
src/theory/theory_model_builder.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/arrays/issue3813-massign-assert.smt2 [new file with mode: 0644] blob