diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2021-04-12 18:51:24 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-13 01:51:24 +0000 |
| commit | ec0daa929c59dbed12ea119f3a5503e37f13d887 (patch) | |
| tree | 7555dc3cb0429bf48d3cfbf873fa29898ca08d9b /test | |
| parent | d5023d8b814b177651d4bb8d09b5818c90fbc7f0 (diff) | |
Fix sexpr bug with AST output language. (#6329)
When a command is invoked, its result/status may be printed depending on its current verbosity, which (for probably an outdated reason) is stored in SMTEngine. One of my previous PRs modified the SMTEngine to return the verbosity as an sexpr. The modification works correctly when the output language is SMT2, but it breaks down with the AST output language, which prints sexprs in a different way. This PR fixes this bug by making SMTEngine return options as strings instead of sexpr.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/options/ast-and-sexpr.smt2 | 17 |
2 files changed, 18 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c40174eda..e84281a0d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -710,6 +710,7 @@ set(regress_0_tests regress0/nl/very-easy-sat.smt2 regress0/nl/very-simple-unsat.smt2 regress0/opt-abd-no-use.smt2 + regress0/options/ast-and-sexpr.smt2 regress0/options/invalid_dump.smt2 regress0/options/set-and-get-options.smt2 regress0/parallel-let.smt2 diff --git a/test/regress/regress0/options/ast-and-sexpr.smt2 b/test/regress/regress0/options/ast-and-sexpr.smt2 new file mode 100644 index 000000000..2a464571c --- /dev/null +++ b/test/regress/regress0/options/ast-and-sexpr.smt2 @@ -0,0 +1,17 @@ +; EXPECT: (SEXPR (SEXPR check-sat (CONST_RATIONAL 2)) (SEXPR * (CONST_RATIONAL 1))) +; EXPECT: (:status unknown) + +; This regression tests uses of s-expressions when the output-language is AST + +(set-option :output-language ast) + +; Set the verbosity of all commands to 1 +(set-option :command-verbosity (* 1)) +; Set the verbosity of (check-sat) command to 2 +(set-option :command-verbosity (check-sat 2)) +; Get the verbosity of all commands +(get-option :command-verbosity) +; There is no SMT option to get the verbosity of a specific command + +(set-info :source (0 1 True False x "")) +(get-info :status) |