From a6de8a73bc6a07a272631638aac16579118ad741 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Thu, 13 Jan 2022 10:11:53 -0800 Subject: [PATCH] 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. --- README.md | 2 +- what4/test/ExprBuilderSMTLib2.hs | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index db0f8a44..c3663451 100644 --- 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 index 73040dfb..3b18fc70 100644 --- 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