Change default smt2 solver to yices (Yices 2 has switched its license to GPL)

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 50ed8c01d7df652079ef0a464b8ce081a32f8c45..a51986065cede47c7d7acc658b41987b21c7a9b7 100644 (file)
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -72,7 +72,7 @@ class SmtIo:
             self.nocomments = opts.nocomments
 
         else:
-            self.solver = "z3"
+            self.solver = "yices"
             self.solver_opts = list()
             self.debug_print = False
             self.debug_file = None
@@ -649,7 +649,7 @@ class SmtOpts:
     def __init__(self):
         self.shortopts = "s:S:v"
         self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
-        self.solver = "z3"
+        self.solver = "yices"
         self.solver_opts = list()
         self.debug_print = False
         self.debug_file = None
@@ -691,8 +691,8 @@ class SmtOpts:
     def helpmsg(self):
         return """
     -s <solver>
-        set SMT solver: z3, cvc4, yices, mathsat, boolector, dummy
-        default: z3
+        set SMT solver: z3, yices, boolector, cvc4, mathsat, dummy
+        default: yices
 
     -S <opt>
         pass <opt> as command line argument to the solver