smtio: Add support for parsing `yosys-smt2-solver-option` info statements.

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 4ac437c36a916c1b9bbbe48fbf14267f69c8b96c..6191eabf6b8f73852677f018d7de7daf34184ce0 100644 (file)
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -124,6 +124,7 @@ class SmtIo:
         self.timeout = 0
         self.produce_models = True
         self.smt2cache = [list()]
+        self.smt2_options = dict()
         self.p = None
         self.p_index = solvers_index
         solvers_index += 1
@@ -258,14 +259,17 @@ class SmtIo:
         for stmt in self.info_stmts:
             self.write(stmt)
 
-        if self.forall and self.solver == "yices":
-            self.write("(set-option :yices-ef-max-iters 1000000000)")
-
         if self.produce_models:
             self.write("(set-option :produce-models true)")
 
         self.write("(set-logic %s)" % self.logic)
 
+        if self.forall and self.solver == "yices":
+            self.write("(set-option :yices-ef-max-iters 1000000000)")
+
+        for key, val in self.smt2_options.items():
+            self.write("(set-option {} {})".format(key, val))
+
     def timestamp(self):
         secs = int(time() - self.start_time)
         return "## %3d:%02d:%02d " % (secs // (60*60), (secs // 60) % 60, secs % 60)
@@ -468,6 +472,9 @@ class SmtIo:
 
         fields = stmt.split()
 
+        if fields[1] == "yosys-smt2-solver-option":
+            self.smt2_options[fields[2]] = fields[3]
+
         if fields[1] == "yosys-smt2-nomem":
             if self.logic is None:
                 self.logic_ax = False