Add smtc option

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index 594f6d79e21c7dd50e1994e6712f28ee6f072451..015f17208e9004f33c32c7f1359c7c7f18b6b5e9 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -435,6 +435,12 @@ class SbyJob:
         self.handle_bool_option("wait", False)
         self.handle_int_option("timeout", None)
 
+        self.handle_str_option("smtc", None)
+
+        if self.opt_smtc is not None:
+            for engine in self.engines:
+                assert engine[0] == "smtbmc"
+
         self.copy_src()
 
         if self.opt_mode == "bmc":

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 392fbea1f61589807630928370a49fd3fe742837..dce23e41a50177560a8d3cde01740b90f2975657 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -40,6 +40,9 @@ def run(mode, job, engine_idx, engine):
     for i, a in enumerate(args):
         smtbmc_opts += ["-s" if i == 0 else "-S", a]
 
+    if job.opt_smtc is not None:
+        smtbmc_opts += ["--smtc", "src/%s" % job.opt_smtc]
+
     model_name = "smt2"
     if syn_opt: model_name += "_syn"
     if nomem_opt: model_name += "_nomem"