diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-04-19 11:47:38 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-19 11:47:38 -0700 |
| commit | 70046d35f2aff41867cbb6490e5bf6d026dc55a1 (patch) | |
| tree | a6903beb73a028ea159b07bb5c773386c1e5c5f5 /test/regress/Makefile.tests | |
| parent | 4af9af22f728ebb12afe48c587cfe665fc8cb123 (diff) | |
Refactor pbRewrites preprocessing pass (#1767)
This commit refactors the pbRewrites preprocessing pass into the new
style. This commit is essentially just a code move and adds a regression
test for the preprocessing pass. It also makes use of the
AssertionPipeline::replace function to do proper dependency tracking.
Diffstat (limited to 'test/regress/Makefile.tests')
| -rw-r--r-- | test/regress/Makefile.tests | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index f41a3a15f..56965f272 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -989,6 +989,7 @@ REG1_TESTS = \ regress1/arith/mod.02.smt2 \ regress1/arith/mod.03.smt2 \ regress1/arith/mult.02.smt2 \ + regress1/arith/pbrewrites-test.smt2 \ regress1/arith/problem__003.smt2 \ regress1/arrayinuf_error.smt2 \ regress1/aufbv/bug580.smt2 \ @@ -1038,6 +1039,7 @@ REG1_TESTS = \ regress1/errorcrash.smt2 \ regress1/fmf-fun-dbu.smt2 \ regress1/fmf/ALG008-1.smt2 \ + regress1/fmf/Hoare-z3.931718.smt \ regress1/fmf/LeftistHeap.scala-8-ncm.smt2 \ regress1/fmf/PUZ001+1.smt2 \ regress1/fmf/agree466.smt2 \ @@ -1065,7 +1067,6 @@ REG1_TESTS = \ regress1/fmf/fore19-exp2-core.smt2 \ regress1/fmf/german169.smt2 \ regress1/fmf/german73.smt2 \ - regress1/fmf/Hoare-z3.931718.smt \ regress1/fmf/issue916-fmf-or.smt2 \ regress1/fmf/jasmin-cdt-crash.smt2 \ regress1/fmf/ko-bound-set.cvc \ |