diff options
| author | Clifford Wolf <clifford@clifford.at> | 2017-01-02 20:02:52 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2017-01-02 20:08:03 +0100 |
| commit | 81bb952e5d2125f3e0700a8a61d2d33297e8b710 (patch) | |
| tree | f753dc4650a7f81332caaa1b2d4050b131152c5c /backends | |
| parent | f0df7dd7961128824baa785a6f76462f36877e4d (diff) | |
| download | yosys-81bb952e5d2125f3e0700a8a61d2d33297e8b710.tar.gz yosys-81bb952e5d2125f3e0700a8a61d2d33297e8b710.tar.bz2 yosys-81bb952e5d2125f3e0700a8a61d2d33297e8b710.zip | |
Handle "always 1" like "always -1" in .smtc files
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/smt2/smtbmc.py | 12 |
1 files changed, 5 insertions, 7 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index dc89b795d..8dbb047aa 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -201,10 +201,9 @@ for fn in inconstr: current_states = set(["final-%d" % i for i in range(0, num_steps+1)]) constr_final_start = 0 elif len(tokens) == 2: - i = int(tokens[1]) - assert i < 0 - current_states = set(["final-%d" % i for i in range(-i, num_steps+1)]) - constr_final_start = -i if constr_final_start is None else min(constr_final_start, -i) + arg = abs(int(tokens[1])) + current_states = set(["final-%d" % i for i in range(arg, num_steps+1)]) + constr_final_start = arg if constr_final_start is None else min(constr_final_start, arg) else: assert False continue @@ -232,9 +231,8 @@ for fn in inconstr: if len(tokens) == 1: current_states = set(range(0, num_steps+1)) elif len(tokens) == 2: - i = int(tokens[1]) - assert i < 0 - current_states = set(range(-i, num_steps+1)) + arg = abs(int(tokens[1])) + current_states = set(range(arg, num_steps+1)) else: assert False continue |