Added fix and test to term translation: now handles escape sequences …

…in string literals and extra quotations.

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(

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);