From 42f3382a266baba0d21486cea6a78f0fc22af516 Mon Sep 17 00:00:00 2001 From: Kevin Quick Date: Wed, 12 Jan 2022 13:38:27 -0800 Subject: [PATCH] [CI] skip and note CVC4 v1.7's many problems --- README.md | 2 +- what4/test/OnlineSolverTest.hs | 18 +++++++++++++++--- 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 134426cc..7cdfcbd0 100644 --- a/README.md +++ b/README.md @@ -20,6 +20,6 @@ views or policies of the Department of Defense or the U.S. Government. | Feature | ABC | Boolector | CVC4 | Dreal | STP | Yices | Z3 | |---------------------------------------|-----|-----------|-------------|-------|----------|----------|-----------------| -| Supported | yes | 3.2.2, ? | 1.7, 1.8, ? | yes | 2.3.3, ? | 2.6.x, ? | 4.8.8 -- 4.8.14 | +| Supported | yes | 3.2.2, ? | >= 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 | diff --git a/what4/test/OnlineSolverTest.hs b/what4/test/OnlineSolverTest.hs index f2a54b04..00813c5c 100644 --- a/what4/test/OnlineSolverTest.hs +++ b/what4/test/OnlineSolverTest.hs @@ -161,10 +161,12 @@ checkFormula1Model sym p q r eval = -- (push/pop) for each of the good and bad cases or else no frames and -- resetting the solver between cases quickstartTest :: Bool -> (SolverTestData,SolverVersion) -> TestTree -quickstartTest useFrames ((SolverName nm, AnOnlineSolver (Proxy :: Proxy s), features, opts, _timeoutOpt),_) = +quickstartTest useFrames ((SolverName nm, AnOnlineSolver (Proxy :: Proxy s), features, opts, _timeoutOpt), SolverVersion sver) = let wrap = if nm == "STP" then ignoreTestBecause "STP cannot generate the model" - else id + else if nm == "CVC4" && any ("1.7" ==) (words sver) + then ignoreTestBecause "CVC4 1.7 non-framed mode fails" + else id in wrap $ testCaseSteps nm $ \step -> withIONonceGenerator $ \gen -> @@ -409,7 +411,17 @@ timeoutTests testLevel solvers = let historical = fromMaybe (0.0 % Second) $ lookup (testSolverName sti) approxTestTimes snamestr (SolverName sname) = sname - in testGroup (snamestr $ testSolverName sti) + maybeSkipTest = + , let maybeRunTest = + case (testSolverName sti, sv) of + -- CVC4 v1.7 generates a response _much_ too + -- quickly (~0.25s). This doesn't allow timeout + -- testing, and the speed suggests an improper + -- result as well. + (SolverName "CVC4", SolverVersion v) | "1.7" `elem` words v-> + ignoreTestBecause "solver completes too quickly" + _ -> id + in maybeRunTest $ testGroup (snamestr $ testSolverName sti) [ testCase ("Test itself is valid and completes (" <> show historical <> ")") $ do -- Verify that the solver will run to completion for