diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-10-20 18:22:55 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-20 18:22:55 -0700 |
| commit | e590612dc4421d45cacc451a7b8a162acd9c7943 (patch) | |
| tree | 4de15750b40cdea6ab8584859b830927897297cf | |
| parent | ea1a513414f0de19a45f58e5e43ccd9c3f290726 (diff) | |
Fix (#7437)
This PR reintroduces support for the (deprecated) option interactive-mode. It was erroneously removed in #7295.
Fixes #7379.
| -rw-r--r-- | src/options/smt_options.toml | 1 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/options/interactive-mode.smt2 | 10 |
3 files changed, 12 insertions, 0 deletions
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 19862cab2..420496190 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -259,6 +259,7 @@ name = "SMT Layer" category = "common" long = "produce-assertions" type = "bool" + alias = ["interactive-mode"] help = "keep an assertions list (enables get-assertions command)" [[option]] diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 0d8123aa3..fca1543c4 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -767,6 +767,7 @@ set(regress_0_tests regress0/nl/very-simple-unsat.smt2 regress0/opt-abd-no-use.smt2 regress0/options/ast-and-sexpr.smt2 + regress0/options/interactive-mode.smt2 regress0/options/invalid_dump.smt2 regress0/options/set-after-init.smt2 regress0/options/set-and-get-options.smt2 diff --git a/test/regress/regress0/options/interactive-mode.smt2 b/test/regress/regress0/options/interactive-mode.smt2 new file mode 100644 index 000000000..549fdfd24 --- /dev/null +++ b/test/regress/regress0/options/interactive-mode.smt2 @@ -0,0 +1,10 @@ +; EXPECT: true +; EXPECT: true +; EXPECT: false +; EXPECT: false +(set-option :interactive-mode true) +(get-option :interactive-mode) +(get-option :produce-assertions) +(set-option :produce-assertions false) +(get-option :interactive-mode) +(get-option :produce-assertions)
\ No newline at end of file |