diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-05-11 08:47:02 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-11 08:47:02 -0700 |
| commit | 1e0ff61c96c455287fd7986ce353dc2754f85d4f (patch) | |
| tree | c7ed06c967361829a9c01c02389cd1cadb2a60c8 /test/regress/Makefile.tests | |
| parent | 5e2366d542e17ba5064a56f2581ada99c0046ddc (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.
Diffstat (limited to 'test/regress/Makefile.tests')
| -rw-r--r-- | test/regress/Makefile.tests | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index 52eb63789..06bec8454 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1017,6 +1017,7 @@ REG1_TESTS = \ regress1/bug516.smt2 \ regress1/bug519.smt2 \ regress1/bug520.smt2 \ + regress1/bug520-eager.smt2 \ regress1/bug521.smt2 \ regress1/bug543.smt2 \ regress1/bug567.smt2 \ |