projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b6ce0f2) | patch
Fix case of uninterpreted constant instantiation in FMF (#3543)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 9 Dec 2019 20:32:32 +0000 (14:32 -0600)
committerAndres Noetzli <andres.noetzli@gmail.com>
Mon, 9 Dec 2019 20:32:32 +0000 (12:32 -0800)
commit33c5eb093a7f032a7d9c9263da595eb53fdd223b
treea08a2ab95bb8e09b6be768b18b99346c48488dectree
parentb6ce0f23ce0aaa0552767e8067fe58dbceee11cbcommit | diff
Fix case of uninterpreted constant instantiation in FMF (#3543)

Fixes #3537.
This benchmark triggers a potential unsoundness caused by instantiating with an uninterpreted constant (which is unsound).
src/theory/quantifiers/fmf/full_model_check.cpp diff | blob | history
src/theory/rep_set.cpp diff | blob | history
src/theory/rep_set.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/quantifiers/issue3537.smt2 [new file with mode: 0644] blob