Run preprocess rewrite on equalities until fixed point (#8291)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 14 Mar 2022 16:56:52 +0000 (11:56 -0500)
committerGitHub <noreply@github.com>
Mon, 14 Mar 2022 16:56:52 +0000 (16:56 +0000)
commit8699e3e95075e262852b57ea9a298648d5caa26c
tree76fed4e15fb8085c82688ecd8507a6fd01f04ba9
parentca89676e63717ebd5ab5b22dc9b8740af9021558
Run preprocess rewrite on equalities until fixed point (#8291)

Previously we were only running once, while strings assumed this was run on what it returned.

This should significantly improve our performance on the benchmarks from SMT-LIB that involving looping word equations.
src/preprocessing/passes/theory_rewrite_eq.cpp
test/regress/CMakeLists.txt
test/regress/regress0/strings/quad-138-4-2-unsat.smt2 [new file with mode: 0644]