Yices: Default to QF_AUFLIA if logic cannot be determined

This is a “heuristic” guess, unlikely to work at all instances, but sufficient enough for most cases.
LeventErkok · Aug 27, 2015 · c71bd2a · c71bd2a
1 parent d423bb9
commit c71bd2a
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/Data/SBV/Provers/Yices.hs b/Data/SBV/Provers/Yices.hs
@@ -27,7 +27,7 @@ yices = SMTSolver {
          , engine       = standardEngine "SBV_YICES" "SBV_YICES_OPTIONS" addTimeOut standardModel
          , capabilities = SolverCapabilities {
                                 capSolverName              = "Yices"
-                              , mbDefaultLogic             = Nothing
+                              , mbDefaultLogic             = Just "QF_AUFLIA"
                               , supportsMacros             = True
                               , supportsProduceModels      = True
                               , supportsQuantifiers        = False

diff --git a/SBVUnitTest/SBVUnitTestBuildTime.hs b/SBVUnitTest/SBVUnitTestBuildTime.hs
@@ -2,4 +2,4 @@
 module SBVUnitTestBuildTime (buildTime) where
 
 buildTime :: String
-buildTime = "Fri Jul 24 15:15:37 PDT 2015"
+buildTime = "Thu Aug 27 01:45:22 PDT 2015"