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 | |
| 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')
| -rw-r--r-- | test/regress/regress0/datatypes/datatype-dump.cvc | 2 | ||||
| -rw-r--r-- | test/regress/regress0/printer/let_shadowing.smt2 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/regress0/datatypes/datatype-dump.cvc b/test/regress/regress0/datatypes/datatype-dump.cvc index e28fc6305..8a193b71a 100644 --- a/test/regress/regress0/datatypes/datatype-dump.cvc +++ b/test/regress/regress0/datatypes/datatype-dump.cvc @@ -1,7 +1,7 @@ % This regression is the same as datatype.cvc but tests the % dumping infrastructure. % -% COMMAND-LINE: --dump raw-benchmark +% COMMAND-LINE: -o raw-benchmark % % EXPECT: OPTION "incremental" false; % EXPECT: OPTION "logic" "ALL"; 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)))))) |