projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: b20f241) | patch
Attempted "quick-fix" for QF_UF performance regression since Boolean terms added.
authorMorgan Deters <mdeters@gmail.com>
Wed, 28 Nov 2012 21:18:05 +0000 (21:18 +0000)
committerMorgan Deters <mdeters@gmail.com>
Wed, 28 Nov 2012 21:18:05 +0000 (21:18 +0000)
commitcce79b9667a4fd067e75d19926b22f0689756daa
tree820c827e2ca1d0dbd38fdad33599ae1fe2eaabd2tree
parentb20f2417722f00f8849d91c1ed8a18599bc17850commit | diff
Attempted "quick-fix" for QF_UF performance regression since Boolean terms added.

Sharing is turned on only when Boolean terms are detected during preprocessing.  QF_UF problems (and others)
that don't use any Boolean terms won't have BV turned on.

(this commit was certified error- and warning-free by the test-and-commit script.)
src/smt/smt_engine.cpp diff | blob | history