Merge pull request #6424 from thomasspriggs/tas/fix_get_value_printing

Fix printing of `smt_get_value_commandt`

Author: thomasspriggs

src/solvers/smt2_incremental/smt_commands.h

@@ -87,6 +87,14 @@ class smt_get_value_commandt : public smt_commandt,
                                protected smt_termt::storert<smt_assert_commandt>
 {
 public:
+  /// \brief This constructor constructs the `get-value` command, such that it
+  ///   stores a single descriptor for which the solver will be commanded to
+  ///   respond with a value.
+  /// \note This class currently supports storing a single descriptor only,
+  ///   whereas the SMT-LIB standard version 2.6 supports one or more
+  ///   descriptors. Getting one value at a time is currently sufficient for our
+  ///   requirements. This class could be expanded should there be a need to get
+  ///   multiple values at once.
   explicit smt_get_value_commandt(smt_termt descriptor);
   const smt_termt &descriptor() const;
 };

src/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -334,7 +334,7 @@ class smt_command_to_string_convertert
 
   void visit(const smt_get_value_commandt &get_value) override
   {
-    os << "(get-value " << get_value.descriptor() << ")";
+    os << "(get-value (" << get_value.descriptor() << "))";
   }
 
   void visit(const smt_pop_commandt &pop) override

unit/solvers/smt2_incremental/smt_to_smt2_string.cpp

@@ -69,6 +69,15 @@ TEST_CASE(
   CHECK(smt_to_smt2_string(smt_exit_commandt{}) == "(exit)");
 }
 
+TEST_CASE(
+  "Test smt_get_value_commandt to string conversion",
+  "[core][smt2_incremental]")
+{
+  CHECK(
+    smt_to_smt2_string(smt_get_value_commandt{
+      smt_identifier_termt{"foo", smt_bool_sortt{}}}) == "(get-value (|foo|))");
+}
+
 TEST_CASE(
   "Test smt_push_commandt to string conversion",
   "[core][smt2_incremental]")