projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5e2366d) | patch
Fix ackermannize preprocessing pass. (#1904)
authorAina Niemetz <aina.niemetz@gmail.com>
Fri, 11 May 2018 15:47:02 +0000 (08:47 -0700)
committerGitHub <noreply@github.com>
Fri, 11 May 2018 15:47:02 +0000 (08:47 -0700)
commit1e0ff61c96c455287fd7986ce353dc2754f85d4f
treec7ed06c967361829a9c01c02389cd1cadb2a60c8tree
parent5e2366d542e17ba5064a56f2581ada99c0046ddccommit | diff
Fix ackermannize preprocessing pass. (#1904)

Ackermannization did not consider cases where UF are Boolean. Model generation is
still not supported, but now guarded against when bit-vectors are combined with arrays
and/or uninterpreted functions and --bitblast=eager.
src/preprocessing/passes/bv_ackermann.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
test/regress/Makefile.tests diff | blob | history
test/regress/regress1/bug520-eager.smt2 [new file with mode: 0644] blob