From ec0daa929c59dbed12ea119f3a5503e37f13d887 Mon Sep 17 00:00:00 2001
From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Mon, 12 Apr 2021 18:51:24 -0700
Subject: 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.
---
 test/regress/CMakeLists.txt | 1 +
 1 file changed, 1 insertion(+)

(limited to 'test/regress/CMakeLists.txt')

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
-- 
cgit v1.2.3