Skip to content

Commit b371c81

Browse files
committed
Fix printing of smt_get_value_commandt
The get value command is supposed to be parameterised with a collection of one or more terms for which the solver should return the values. Our internal representation of the get-value command only supports a single term, which should be placed in brackets to make it into a collection containing a single term. The brackets were previously missing, which would have caused a solver error.
1 parent 33c909b commit b371c81

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

src/solvers/smt2_incremental/smt_to_smt2_string.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -334,7 +334,7 @@ class smt_command_to_string_convertert
334334

335335
void visit(const smt_get_value_commandt &get_value) override
336336
{
337-
os << "(get-value " << get_value.descriptor() << ")";
337+
os << "(get-value (" << get_value.descriptor() << "))";
338338
}
339339

340340
void visit(const smt_pop_commandt &pop) override

unit/solvers/smt2_incremental/smt_to_smt2_string.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ TEST_CASE(
7575
{
7676
CHECK(
7777
smt_to_smt2_string(smt_get_value_commandt{
78-
smt_identifier_termt{"foo", smt_bool_sortt{}}}) == "(get-value |foo|)");
78+
smt_identifier_termt{"foo", smt_bool_sortt{}}}) == "(get-value (|foo|))");
7979
}
8080

8181
TEST_CASE(

0 commit comments

Comments
 (0)