diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-05-11 11:49:45 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-05-11 11:49:45 -0700 |
| commit | d74fae48252f04de4e72ed5337b1bf62c234d0fd (patch) | |
| tree | 430f0b6266a89638c071f386a2ff3413862320ba /test/regress/regress1/bug520.smt2 | |
| parent | 1e0ff61c96c455287fd7986ce353dc2754f85d4f (diff) | |
Remove obsolete unit test for ackermannization. (#1906)
With #1902, test/regress/regress1/bug520-eager.smt2 is now obsolete.
Diffstat (limited to 'test/regress/regress1/bug520.smt2')
| -rw-r--r-- | test/regress/regress1/bug520.smt2 | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/test/regress/regress1/bug520.smt2 b/test/regress/regress1/bug520.smt2 index 4bdb968d8..0965487e1 100644 --- a/test/regress/regress1/bug520.smt2 +++ b/test/regress/regress1/bug520.smt2 @@ -1,5 +1,7 @@ +; COMMAND-LINE: --bitblast=lazy +; COMMAND-LINE: --bitblast=eager --no-check-models +; EXPECT: sat ; Automatically generated by SBV. Do not edit. -(set-option :produce-models true) (set-logic QF_UFBV) (set-info :status sat) ; --- uninterpreted sorts --- |