Skip to content

Commit 9aaefaf

Browse files
Strings: Fix evaluation of Unicode String formulas in ModelEvaluationTest
1 parent 06232f9 commit 9aaefaf

File tree

1 file changed

+6
-1
lines changed

1 file changed

+6
-1
lines changed

src/org/sosy_lab/java_smt/test/ModelEvaluationTest.java

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@
2525
import org.sosy_lab.java_smt.api.ProverEnvironment;
2626
import org.sosy_lab.java_smt.api.SolverContext.ProverOptions;
2727
import org.sosy_lab.java_smt.api.SolverException;
28+
import org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager;
2829

2930
/** Test that we can request evaluations from models. */
3031
public class ModelEvaluationTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 {
@@ -168,7 +169,11 @@ public void testGetStringsEvaluation() throws SolverException, InterruptedExcept
168169

169170
// Unicode
170171
evaluateInModel(
171-
smgr.equal(smgr.makeVariable("x"), smgr.makeString("hello æ@€ \u1234 \\u{4321}")),
172+
smgr.equal(
173+
smgr.makeVariable("x"),
174+
smgr.makeString(
175+
AbstractStringFormulaManager.unescapeUnicodeForSmtlib(
176+
"hello æ@€ \u1234 \\u{4321}"))),
172177
smgr.makeVariable("x"),
173178
Lists.newArrayList("hello \u00e6@\u20ac \u1234 \u4321"),
174179
Lists.newArrayList(smgr.makeString("hello \u00e6@\u20ac \u1234 \u4321")));

0 commit comments

Comments
 (0)