diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-09-14 10:31:07 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-09-14 15:31:07 +0000 |
commit | efdefd95abd7de85963b9dd22e98e2858864cb07 (patch) | |
tree | 1108123b3f08ac66d6db5a002955891e9a398809 /test/regress/regress0/printer | |
parent | a37f486c6e10b882a81474418e1d3f4ffdbd583c (diff) |
Reimplement `--dump=raw-benchmark` as `-o raw-benchmark` (#7191)
Printing the original benchmark is simple, as it is exactly the commands we execute.
This removes the previous code from SmtEngine, which is currently broken.
Diffstat (limited to 'test/regress/regress0/printer')
-rw-r--r-- | test/regress/regress0/printer/let_shadowing.smt2 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress0/printer/let_shadowing.smt2 b/test/regress/regress0/printer/let_shadowing.smt2 index 02eb3376a..fbea9d142 100644 --- a/test/regress/regress0/printer/let_shadowing.smt2 +++ b/test/regress/regress0/printer/let_shadowing.smt2 @@ -1,5 +1,5 @@ ; REQUIRES: dumping -; COMMAND-LINE: --dump raw-benchmark --preprocess-only +; COMMAND-LINE: -o raw-benchmark --preprocess-only ; SCRUBBER: grep assert ; EXPECT: (assert (let ((_let_1 (* x y))) (and (= _let_1 _let_1) (= _let_1 _let_0)))) ; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((_let_0 Int)) (= 0 _let_0)))))) |