projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 42f4798) | patch
Generalize LFSC concat unify for splitting constants (#8077)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 7 Feb 2022 23:44:06 +0000 (17:44 -0600)
committerGitHub <noreply@github.com>
Mon, 7 Feb 2022 23:44:06 +0000 (17:44 -0600)
commit953906062c77984cca9930fe3c4d015388f9ca86
tree1c8a969377c29748e1082f31e049420f59c3d1e1tree
parent42f4798be4268e65b04d54b5711f5ca896b333edcommit | diff
Generalize LFSC concat unify for splitting constants (#8077)

Was causing LFSC proof failures on ~5 SMT-LIB strings benchmarks.
proofs/lfsc/signatures/nary_programs.plf diff | blob | history
proofs/lfsc/signatures/strings_programs.plf diff | blob | history
proofs/lfsc/signatures/strings_rules.plf diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/strings/instance6561-dd-concat-unify-char.smt2 [new file with mode: 0644] blob