Support building with sbv-10.* (#1523)

`sbv-10.0` brings in two changes to the SBV internals that affect Cryptol.

1. `sbv-10.0` removes the `generateSMTBenchmark` function in favor of two
   separate `generateSMTBenchmarkSat` and `generateSMTBenchmarkProof` functions.
2. `sbv-10.0` removes the `allSatHasPrefixExistentials` field of `AllSatResult`.

We now use the appropriate CPP to make Cryptol compile before and after these
changes.

Fixes #1513.

cryptol.cabal

@@ -73,7 +73,7 @@ library
                        pretty,
                        prettyprinter     >= 1.7.0,
                        process           >= 1.2,
-                       sbv               >= 9.1 && < 9.3,
+                       sbv               >= 9.1 && < 10.2,
                        simple-smt        >= 0.9.7,
                        stm               >= 2.4,
                        strict,

src/Cryptol/Symbolic/SBV.hs

@@ -411,7 +411,10 @@ processResults ProverCommand{..} ts results =
 
        -- otherwise something is wrong
        _ -> return $ ProverError (rshow results)
-#if MIN_VERSION_sbv(8,8,0)
+#if MIN_VERSION_sbv(10,0,0)
+              where rshow | isSat = show . (SBV.AllSatResult False False False)
+                    -- sbv-10.0.0 removes the `allSatHasPrefixExistentials` field
+#elif MIN_VERSION_sbv(8,8,0)
               where rshow | isSat = show . (SBV.AllSatResult False False False False)
 #else
               where rshow | isSat = show .  SBV.AllSatResult . (False,False,False,)
@@ -466,11 +469,19 @@ satProveOffline _proverCfg pc@ProverCommand {..} =
               ProveQuery -> False
               SafetyQuery -> False
               SatQuery _ -> True
+
+#if MIN_VERSION_sbv(10,0,0)
+            generateSMTBenchmark
+              | isSat     = SBV.generateSMTBenchmarkSat
+              | otherwise = SBV.generateSMTBenchmarkProof
+#else
+            generateSMTBenchmark = SBV.generateSMTBenchmark isSat
+#endif
         evo <- liftIO (M.minpEvalOpts minp)
 
         prepareQuery evo pc >>= \case
           Left msg -> return (Left msg)
-          Right (_ts, q) -> Right <$> M.io (SBV.generateSMTBenchmark isSat q)
+          Right (_ts, q) -> Right <$> M.io (generateSMTBenchmark q)
 
 protectStack :: (String -> M.ModuleCmd a)
              -> M.ModuleCmd a