[CI] skip and note CVC4 v1.7's many problems

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       |

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