From: Gereon Kremer <nafur42@gmail.com>
Date: Thu, 21 Oct 2021 01:22:55 +0000 (-0700)
Subject: Fix (#7437)
X-Git-Tag: cvc5-1.0.0~1024
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e590612dc4421d45cacc451a7b8a162acd9c7943;p=cvc5.git

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 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