Handle "always 1" like "always -1" in .smtc files

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index dc89b795d59ceca166b34b3d84f5e28b7af402b3..8dbb047aa457401bf55d216288864f0b5d3d236d 100644 (file)
--- 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