improve unit test for allChar.

sosy-lab · Sep 15, 2022 · ae3a80b · ae3a80b
1 parent 0c32514
commit ae3a80b
Showing 1 changed file with 9 additions and 8 deletions.
diff --git a/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/StringFormulaManagerTest.java
@@ -148,23 +148,24 @@ public void testRegexAllChar() throws SolverException, InterruptedException {
   public void testRegexAllCharUnicode() throws SolverException, InterruptedException {
     RegexFormula regexAllChar = smgr.allChar();
 
-    if (solverUnderTest == Solvers.CVC4) {
-      // CVC4 does not support Unicode characters
-      assertThatFormula(smgr.in(smgr.makeString("\\u0394"), regexAllChar)).isUnsatisfiable();
+    // Single characters.
+    assertThatFormula(smgr.in(smgr.makeString("\\u0394"), regexAllChar)).isSatisfiable();
+    assertThatFormula(smgr.in(smgr.makeString("\\u{1fa6a}"), regexAllChar)).isSatisfiable();
 
-    } else {
+    // Combining characters are not matched as one character.
+    assertThatFormula(smgr.in(smgr.makeString("a\\u0336"), regexAllChar)).isUnsatisfiable();
+    assertThatFormula(smgr.in(smgr.makeString("\\n"), regexAllChar)).isUnsatisfiable();
+
+    if (solverUnderTest != Solvers.CVC4) {
+      // CVC4 does not support Unicode characters.
       // Z3 and other solvers support Unicode characters in the theory of strings.
-      assertThatFormula(smgr.in(smgr.makeString("\\u0394"), regexAllChar)).isSatisfiable();
-      assertThatFormula(smgr.in(smgr.makeString("\\u{1fa6a}"), regexAllChar)).isSatisfiable();
       assertThatFormula(
               smgr.in(
                   smgr.makeVariable("x"), smgr.intersection(smgr.range('a', 'Δ'), regexAllChar)))
           .isSatisfiable();
       // Combining characters are not matched as one character.
-      assertThatFormula(smgr.in(smgr.makeString("a\\u0336"), regexAllChar)).isUnsatisfiable();
       // Non-ascii non-printable characters should use the codepoint representation
       assertThatFormula(smgr.in(smgr.makeString("Δ"), regexAllChar)).isUnsatisfiable();
-      assertThatFormula(smgr.in(smgr.makeString("\\n"), regexAllChar)).isUnsatisfiable();
     }
   }