From 86b16e3f38be421a5bb5a1aa87dfdf970ea3fcdb Mon Sep 17 00:00:00 2001 From: Thomas Given-Wilson Date: Mon, 28 Jun 2021 14:52:16 +0100 Subject: [PATCH] Fix quoting for object size identifiers in SMT2 output This puts correct quoting around the object size identifiers in the SMT2 output code. --- src/solvers/smt2/smt2_conv.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp index d9da852ab62..bcaf8f1d5b0 100644 --- a/src/solvers/smt2/smt2_conv.cpp +++ b/src/solvers/smt2/smt2_conv.cpp @@ -258,7 +258,7 @@ void smt2_convt::define_object_size( << "((_ extract " << h << " " << l << ") "; convert_expr(ptr); out << ") (_ bv" << number << " " << config.bv_encoding.object_bits << "))" - << "(= " << id << " (_ bv" << *object_size << " " << size_width + << "(= |" << id << "| (_ bv" << *object_size << " " << size_width << "))))\n"; ++number; @@ -1931,7 +1931,7 @@ void smt2_convt::convert_expr(const exprt &expr) } else if(expr.id()==ID_object_size) { - out << object_sizes[expr]; + out << "|" << object_sizes[expr] << "|"; } else if(expr.id()==ID_let) { @@ -4589,7 +4589,7 @@ void smt2_convt::find_symbols(const exprt &expr) { const irep_idt id = "object_size." + std::to_string(object_sizes.size()); - out << "(declare-fun " << id << " () "; + out << "(declare-fun |" << id << "| () "; convert_type(expr.type()); out << ")" << "\n";