projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 36af095) | patch
Fix quantifiers scope issue in strings preprocessor (#5491)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 23 Nov 2020 01:41:23 +0000 (19:41 -0600)
committerGitHub <noreply@github.com>
Mon, 23 Nov 2020 01:41:23 +0000 (17:41 -0800)
commit2b4d6997eec82dce3832a449eea00f94af420f8a
tree2f59ae07705167fba5db7f7cf8582fa8b69dccedtree
parent36af095242f2445fa5d3c2c1f3882159119d152acommit | diff
Fix quantifiers scope issue in strings preprocessor (#5491)

Leads to free variables in assertions when using `str.<=` whose reduction uses EXISTS not FORALL.

Fixes #5483.
src/theory/strings/theory_strings_preprocess.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/strings/issue5483-pp-leq.smt2 [new file with mode: 0644] blob