From e590612dc4421d45cacc451a7b8a162acd9c7943 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 20 Oct 2021 18:22:55 -0700 Subject: [PATCH] Fix (#7437) This PR reintroduces support for the (deprecated) option interactive-mode. It was erroneously removed in #7295. Fixes #7379. --- src/options/smt_options.toml | 1 + test/regress/CMakeLists.txt | 1 + test/regress/regress0/options/interactive-mode.smt2 | 10 ++++++++++ 3 files changed, 12 insertions(+) create mode 100644 test/regress/regress0/options/interactive-mode.smt2 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 -- 2.30.2