Use new version of SBV

[BinderDavid]

This is the current version of the patch. The core change happens in compileQuantScoped

-compileQuantScoped :: SymVal a => Quantifier -> String -> (SBV a -> Symbolic SBool) -> Symbolic SBool
-compileQuantScoped ForallQ  s = universal [s]
-compileQuantScoped BoundQ   s = universal [s]
-compileQuantScoped _ s = existential [s]
+compileQuantScoped :: SymVal a => Quantifier -> String -> (SBV a -> SBool) -> SBool
+compileQuantScoped ForallQ   _s k = quantifiedBool $ \(Data.SBV.Forall x) -> k x
+compileQuantScoped BoundQ    _s k = quantifiedBool $ \(Data.SBV.Forall x) -> k x
+compileQuantScoped InstanceQ _s k = quantifiedBool $ \(Data.SBV.Exists x) -> k x

which requires changing all monadic code which produces Symbolic SBool to non-monadic code which produces just SBool.

Unfortunately, this generates SMT problems for Z3 that currently timeout in a lot of cases. This needs some further investigation...