Fix CVC5 list parsing

[LeventErkok]

This example:

{-# LANGUAGE OverloadedStrings #-}

import Data.SBV
import qualified Data.SBV.List as L

problemString :: ConstraintSet
problemString = do test :: SList String <- sList "test"
                   constrain $ "US" `L.elem` test
                   constrain $ "EN" `L.elem` test

problemInt :: ConstraintSet
problemInt = do test :: SList Integer <- sList "test"
                constrain $ 1 `L.elem` test
                constrain $ 2 `L.elem` test

test :: IO ()
test = do solve z3   "Z3,   Int"     problemInt
          solve cvc5 "CVC5, Int"     problemInt
          solve z3   "Z3,   String:" problemString
          solve cvc5 "CVC5, String:" problemString
  where solve solver what problem = do putStrLn $ "== " ++ what ++ " version:"
                                       print =<< satWith solver problem

Yields:

*Main> test
== Z3,   Int version:
Satisfiable. Model:
  test = [2,1] :: [Integer]
== CVC5, Int version:
*** Exception: Expected a sequence constant, but received: EApp [ECon "str.++",EApp [ECon "seq.unit",ENum (1,Nothing)],EApp [ECon "seq.unit",ENum (2,Nothing)]]
CallStack (from HasCallStack):
  error, called at ./Data/SBV/Control/Utils.hs:1017:64 in sbv-10.5-2fed672a:Data.SBV.Control.Utils

Because SBV doesn't quite understand CVC5's response here. We should be able to fix this in the SExpr parser.

[LeventErkok]

Looks like this is actually a bug in CVC5. Reported here: https://github.com/cvc5/cvc5/issues/10478

[LeventErkok]

Fixed upstream; no SBV action needed.