GaloisInc/what4
1
1
Fork 0
mirror of https://github.com/GaloisInc/what4.git synced 2024-10-06 00:22:49 +03:00
Code Issues Projects Releases Wiki Activity

Z3 4.8.11 passes string tests.

Browse Source
This commit is contained in:
Kevin Quick 2022-04-05 00:09:47 -07:00
parent 255cbdbef8
commit 82a6d7a74e
No known key found for this signature in database
GPG Key ID: E6D7733599CC0A21
1 changed files with 7 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

14
what4/test/ExprBuilderSMTLib2.hs
View File

@ -1195,9 +1195,9 @@ main = do
solvers <- reportSolverVersions testLevel id
=<< (zip solverNames <$> mapM getSolverVersion solverNames)
let z3Tests =
let skipPre4_8_12 why =
let skipPre4_8_11 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
incompatZ3Strings = "unicode and string escaping not supported for older Z3 versions; upgrade to at least 4.8.11"
@ -1224,12 +1224,12 @@ main = do
, testCase "Z3 pair" $ withOnlineZ3 pairTest
, testCase "Z3 forall binder" $ withOnlineZ3 forallTest
, skipPre4_8_12 incompatZ3Strings $ testCase "Z3 string1" $ withOnlineZ3 stringTest1
, skipPre4_8_11 incompatZ3Strings $ testCase "Z3 string1" $ withOnlineZ3 stringTest1
, testCase "Z3 string2" $ withOnlineZ3 stringTest2
, skipPre4_8_12 incompatZ3Strings $ testCase "Z3 string3" $ withOnlineZ3 stringTest3
, skipPre4_8_12 incompatZ3Strings $ testCase "Z3 string4" $ withOnlineZ3 stringTest4
, skipPre4_8_12 incompatZ3Strings $ testCase "Z3 string5" $ withOnlineZ3 stringTest5
, skipPre4_8_12 incompatZ3Strings $ testCase "Z3 string6" $ withOnlineZ3 stringTest6
, skipPre4_8_11 incompatZ3Strings $ testCase "Z3 string3" $ withOnlineZ3 stringTest3
, skipPre4_8_11 incompatZ3Strings $ testCase "Z3 string4" $ withOnlineZ3 stringTest4
, skipPre4_8_11 incompatZ3Strings $ testCase "Z3 string5" $ withOnlineZ3 stringTest5
, skipPre4_8_11 incompatZ3Strings $ testCase "Z3 string6" $ withOnlineZ3 stringTest6
-- this test apparently passes on older Z3 despite the escaping changes...
, testCase "Z3 string7" $ withOnlineZ3 stringTest7