projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1ba6da8) | patch
Do not split on cardinality for string equivalence classes with non-constant lengths...
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 10 May 2017 15:35:38 +0000 (10:35 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 10 May 2017 15:35:38 +0000 (10:35 -0500)
commitb045d1d06f2d28957ccca6ed7d9e6458b4a96b79
treebb140dd1947f28d1bb41bc5fdc7cdc3e825e9f8btree
parent1ba6da827023f0980ad5a00772dd91665620d2a4commit | diff
Do not split on cardinality for string equivalence classes with non-constant lengths if disequalities already imply sufficient lower bound. Fixes bug 799.
src/theory/strings/theory_strings.cpp diff | blob | history
test/regress/regress0/strings/Makefile.am diff | blob | history
test/regress/regress0/strings/bug799-min.smt2 [new file with mode: 0644] blob