diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2021-03-18 13:33:47 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-18 13:33:47 -0500 |
| commit | 2638e65d242fa9da99d038db07c4a2b75e8dfde3 (patch) | |
| tree | a3be9ecd4d807957e8b0755368707158ca2b79f0 /test/regress | |
| parent | d52bc44199583e3c06816c1d30f61e8075820c1b (diff) | |
Eliminate more uses of SExpr. (#6149)
This PR eliminates all remaining uses of SExpr outside of statistics.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/options/set-and-get-options.smt2 | 19 |
2 files changed, 20 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 14752f726..964e73fc0 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -707,6 +707,7 @@ set(regress_0_tests regress0/nl/very-simple-unsat.smt2 regress0/opt-abd-no-use.smt2 regress0/options/invalid_dump.smt2 + regress0/options/set-and-get-options.smt2 regress0/parallel-let.smt2 regress0/parser/as.smt2 regress0/parser/bv_arity_smt2.6.smt2 diff --git a/test/regress/regress0/options/set-and-get-options.smt2 b/test/regress/regress0/options/set-and-get-options.smt2 new file mode 100644 index 000000000..478e3d523 --- /dev/null +++ b/test/regress/regress0/options/set-and-get-options.smt2 @@ -0,0 +1,19 @@ +; EXPECT: ((* 2)) +; EXPECT: ((check-sat 1) (* 1)) +; EXPECT: true +; EXPECT: false +; EXPECT: 15 +; EXPECT: "SimplificationMode::NONE" + +(get-option :command-verbosity) +(set-option :command-verbosity (* 1)) +(set-option :command-verbosity (check-sat 1)) +(get-option :command-verbosity) +(set-option :check-models true) +(get-option :check-models) +(set-option :check-models false) +(get-option :check-models) +(set-option :dag-thresh 15) +(get-option :dag-thresh) +(set-option :simplification none) +(get-option :simplification) |