projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 67e5e3d) | patch
Remove skolem share involving pre_first_ctn. (#4423)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 30 Apr 2020 23:48:21 +0000 (18:48 -0500)
committerGitHub <noreply@github.com>
Thu, 30 Apr 2020 23:48:21 +0000 (16:48 -0700)
commit0c402c2b3cc036748c83bd75629e9845f9b5a397
tree8a77f78f4db9cf1002616efc4fdb3bd83506da40tree
parent67e5e3d2cf5e381bde65683b1244d1905e969a90commit | diff
Remove skolem share involving pre_first_ctn. (#4423)

This fixes a soundness issue in strings caused by an incorrect skolem share.

This adds a regression that corresponds to the rewrite that this skolem share was justified by, which is "sat" (the rewrite does not hold). This benchmark in fact was answered "unsat" by CVC4 prior to this PR.
src/theory/strings/skolem_cache.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/strings/pre_ctn_no_skolem_share.smt2 [new file with mode: 0644] blob
test/unit/theory/theory_strings_skolem_cache_black.h diff | blob | history