projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 770d9ae) | patch
Disable cegqi-bv when using sygus (#5124)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 23 Sep 2020 19:56:52 +0000 (14:56 -0500)
committerGitHub <noreply@github.com>
Wed, 23 Sep 2020 19:56:52 +0000 (14:56 -0500)
commitaacc90c1234c488f49814fae6dbf0e720e2dfa88
tree4d147316d0d8e8d570f96c43d4f03bba9d0db06atree
parent770d9ae622ec04bc2fbea8356ce11329ed06fa5bcommit | diff
Disable cegqi-bv when using sygus (#5124)

This disables the CAV 2018 techniques for BV quantifier instantiation when solving sygus since they may generate terms with witness in them. This adds a regression where this occurs.

I've opened an cvc4 projects issue to revisit this (CVC4/cvc4-projects#227).
src/smt/set_defaults.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/sygus/find_inv_eq_bvmul_4bit_withoutgrammar-v2.sy [new file with mode: 0644] blob
test/regress/regress1/sygus/max2-bv.sy diff | blob | history