projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1c382bb) | patch
Fix getModelValue for arithmetic (#8316)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 16 Mar 2022 01:11:55 +0000 (20:11 -0500)
committerGitHub <noreply@github.com>
Wed, 16 Mar 2022 01:11:55 +0000 (01:11 +0000)
commit4a8d2407468eee50c91fc6cbe19f5edd8feeb688
tree4da841af8742e75830ea44f863ecdf8d00225053tree
parent1c382bb55e11c383285e188db6fa30a51af8b556commit | diff
Fix getModelValue for arithmetic (#8316)

Fixes #8276.

Theory::getModelValue is used as an optimization for computing the care graph of arrays. This method was wrong for (non-linear) arithmetic when the NL extension repaired values in the model.
src/theory/arith/theory_arith.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/arrays/issue8276-arith-getModelValue.smt2 [new file with mode: 0644] blob