Commit ef02c249 authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Fix bug. It doesn't solve the problem however.

parent db4e3308
......@@ -83,12 +83,11 @@ class RegisterAutomatonBuilder():
start_state = translator.z3_to_state(z3state)
enabled_z3regs = [reg for reg in enabled_z3guards if reg is not self.ra.fresh]
for (z3end_state, z3guards) in z3end_state_to_guards.items():
# a transition which makes an assignment is never merged
if self.ra.fresh in z3guards and update is not self.ra.fresh:
self._add_transition(translator, mut_ra, start_state, z3label,
z3guards, update, z3end_state, enabled_z3regs)
[self.ra.fresh], update, z3end_state, enabled_z3regs)
if len(z3guards) > 0:
self._add_transition(translator, mut_ra, start_state, z3label,
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment