From d9201b85f3eb955af9168a8c6525415f44f64f05 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 27 May 2017 11:56:01 +0200
Subject: [PATCH] Change default smt2 solver to yices (Yices 2 has switched its
 license to GPL)

---
 backends/smt2/smtio.py | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 50ed8c01d..a51986065 100644
--- 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
-- 
2.30.2