Fix (#7437)

This PR reintroduces support for the (deprecated) option interactive-mode. It was erroneously removed in #7295.

Fixes #7379.

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 19862cab2ad0b056f39461005cd3d4efcd279637..42049619001836f2c8b7c63d3c40ce22148886af 100644 (file)
--- 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 0d8123aa364c41a584c217342f702be1491c9cb0..fca1543c41ffdc83242a25502de398e1a8f8c342 100644 (file)
--- 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 (file)
index 0000000..549fdfd
--- /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