Strings: Disable non-BMP test for CVC5 due to a bug in the solver

daniel-raffler · daniel-raffler · commit 226515298020 · 2025-02-27T17:37:34.000+01:00
diff --git a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java
@@ -148,7 +148,7 @@ public void testOutputUnescape() throws SolverException, InterruptedException {
             .isEqualTo("\\u{39E}");
 
         // Test with a character that is not in the BMP
-        if (solver != Solvers.PRINCESS) {
+        if (solver != Solvers.PRINCESS && solver != Solvers.CVC5) {
           String str = Character.toString(0x200cb);
           assertThat(model.evaluate(smgr.makeString(str))).isEqualTo(str);
         }

Original file line number	Diff line number	Diff line change
`@@ -148,7 +148,7 @@ public void testOutputUnescape() throws SolverException, InterruptedException {`
`148`	`148`	`.isEqualTo("\\u{39E}");`
`149`	`149`
`150`	`150`	`// Test with a character that is not in the BMP`
`151`		`- if (solver != Solvers.PRINCESS) {`
	`151`	`+ if (solver != Solvers.PRINCESS && solver != Solvers.CVC5) {`
`152`	`152`	`String str = Character.toString(0x200cb);`
`153`	`153`	`assertThat(model.evaluate(smgr.makeString(str))).isEqualTo(str);`
`154`	`154`	`}`