diff options
author | Clifford Wolf <clifford@clifford.at> | 2017-05-27 11:56:01 +0200 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2017-05-27 11:56:01 +0200 |
commit | d9201b85f3eb955af9168a8c6525415f44f64f05 (patch) | |
tree | 5fba0149cb5d666221d5356b64b8205caf0f05af | |
parent | fad52abf70a056007ef82f91a496c84de149d54a (diff) | |
download | yosys-d9201b85f3eb955af9168a8c6525415f44f64f05.tar.gz yosys-d9201b85f3eb955af9168a8c6525415f44f64f05.tar.bz2 yosys-d9201b85f3eb955af9168a8c6525415f44f64f05.zip |
Change default smt2 solver to yices (Yices 2 has switched its license to GPL)
-rw-r--r-- | backends/smt2/smtio.py | 8 |
1 files 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 |