From 630c66c4d316196299cdce1eb2f1e23562a19d36 Mon Sep 17 00:00:00 2001
From: Rachel <rachel.cleaveland@gmail.com>
Date: Fri, 22 Nov 2024 12:38:52 -0800
Subject: [PATCH] Added fix and test to term translation: now handles escape
 sequences in string literals and extra quotations.

---
 src/term_translator.cpp         |  6 +++++-
 tests/test-term-translation.cpp | 15 +++++++++++++++
 2 files changed, 20 insertions(+), 1 deletion(-)

diff --git a/src/term_translator.cpp b/src/term_translator.cpp
index 503b1c4fb..1ab5dc41b 100644
--- a/src/term_translator.cpp
+++ b/src/term_translator.cpp
@@ -450,7 +450,11 @@ Term TermTranslator::value_from_smt2(const std::string val,
     }
   }
   else if (sk == STRING){
-    return solver->make_term(val, false, sort);
+    std::string new_val = val;
+    if (val.length() > 1 && val.at(0) == '\"') {
+      new_val = new_val.substr(1,new_val.length()-2);
+    }
+    return solver->make_term(new_val, true, sort);
   }
   {
     throw NotImplementedException(
diff --git a/tests/test-term-translation.cpp b/tests/test-term-translation.cpp
index becbbf85d..ceae9c45b 100644
--- a/tests/test-term-translation.cpp
+++ b/tests/test-term-translation.cpp
@@ -294,6 +294,21 @@ TEST_P(TranslationTests, UninterpretedSort)
   EXPECT_EQ(fv, fv_1);
 }
 
+TEST_P(TranslationTests, Strings)
+{
+  Sort strsort = s1->make_sort(STRING);
+  Term t = s1->make_term("\\u{a}", true, strsort);
+
+  TermTranslator to_s2(s2);
+  TermTranslator to_s1(s1);
+
+  Term t2 = to_s2.transfer_term(t);
+  EXPECT_EQ(t2->to_string(), t->to_string());
+
+  Term t1 = to_s1.transfer_term(t2);
+  EXPECT_EQ(t, t1);
+}
+
 TEST_P(BoolArrayTranslationTests, Arrays)
 {
   Term f = s1->make_term(false);