Z3 4.8.11 is capable of supporting unicode strings and escapes.

This was previously mis-identified because the Z3 4.8.11 test configuration was accidentally using Z3 4.8.10.
GaloisInc · Jan 13, 2022 · a6de8a7 · a6de8a7
1 parent 085811c
commit a6de8a7
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/README.md b/README.md
@@ -22,4 +22,4 @@ views or policies of the Department of Defense or the U.S. Government.
 |---------------------------------------|-----|-------------|-----------|-------|-------------|----------|-----------------|
 | Supported                             | yes | >= 3.2.0, ? | >= 1.8, ? | yes   | >= 2.3.3, ? | 2.6.x, ? | 4.8.8 -- 4.8.14 |
 | goal timeouts                         | ?   | yes         | yes       | ?     | yes         | yes      | ! 4.8.12        |
-| strings with unicode and escape codes | ?   | ?           | >= 1.8    | ?     | ?           | ?        | >= 4.8.12       |
+| strings with unicode and escape codes | ?   | ?           | >= 1.8    | ?     | ?           | ?        | >= 4.8.11       |
diff --git a/what4/test/ExprBuilderSMTLib2.hs b/what4/test/ExprBuilderSMTLib2.hs
@@ -1036,10 +1036,10 @@ main = do
   let z3Tests =
         let skipPre4_8_12 why =
               let shouldSkip = case lookup (SolverName "z3") solvers of
-                    Just (SolverVersion v) -> any (`elem` [ "4.8.8", "4.8.9", "4.8.10", "4.8.11" ]) $ words v
+                    Just (SolverVersion v) -> any (`elem` [ "4.8.8", "4.8.9", "4.8.10" ]) $ words v
                     Nothing -> True
               in if shouldSkip then expectFailBecause why else id
-            unsuppStrings = "unicode and string escaping not supported for older Z3 versions; upgrade to at least 4.8.12"
+            unsuppStrings = "unicode and string escaping not supported for older Z3 versions; upgrade to at least 4.8.11"
         in
         [
           testUninterpretedFunctionScope