Disable unrolling per default for z3

diff --git a/docs/examples/multiclk/dpmem.sby b/docs/examples/multiclk/dpmem.sby
index 08e44a6c716a5ca79e91bc1e9048bff919f82a29..574e79eeb98bc4f2d27f5822b5561f28ee8e0f52 100644 (file)
--- a/docs/examples/multiclk/dpmem.sby
+++ b/docs/examples/multiclk/dpmem.sby
@@ -8,7 +8,6 @@ smtbmc
 [script]
 read_verilog -sv -formal dpmem.sv
 prep -nordff -top top
-memory_map
 chformal -early -assume
 clk2fflogic
 opt_clean

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 715404a2abe8433f92e9475f344fdee44ac3b0d3..690dfcc28ec87012334c9c95d69d8ac9064682b3 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -23,7 +23,7 @@ def run(mode, job, engine_idx, engine):
     smtbmc_opts = []
     nomem_opt = False
     presat_opt = True
-    unroll_opt = True
+    unroll_opt = None
     syn_opt = False
     stbv_opt = False
     dumpsmt2 = False
@@ -50,15 +50,17 @@ def run(mode, job, engine_idx, engine):
         else:
             assert False
 
+    for i, a in enumerate(args):
+        if i == 0 and a == "z3" and unroll_opt is None:
+                unroll_opt = False
+        smtbmc_opts += ["-s" if i == 0 else "-S", a]
+
     if presat_opt:
         smtbmc_opts += ["--presat"]
 
-    if unroll_opt:
+    if unroll_opt is None or unroll_opt:
         smtbmc_opts += ["--unroll"]
 
-    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]