fixing qlrf_bg

jesusjda · Sep 13, 2020 · b2080b3 · b2080b3
1 parent 318c7c6
commit b2080b3
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/termination/algorithm/qlrf.py b/termination/algorithm/qlrf.py
@@ -192,7 +192,7 @@ def run(self, cfg, different_template=False, dt_scheme="default"):
         dfs = {}
         for tr in transitions:
             rf_s = rfs[tr["source"]]
-            rf_t = rfs[tr["target"]]
+            rf_t = rfs[tr["target"]].renamed(gvs[:Nvars], gvs[Nvars:])
             poly = tr["polyhedron"]
             df = rf_s - rf_t  # ExprTerm(0)
             constant = (rf_s.get_coeff() - rf_t.get_coeff())
@@ -211,8 +211,8 @@ def run(self, cfg, different_template=False, dt_scheme="default"):
             for tr in transitions:
                 poly = tr["polyhedron"]
                 cons = poly.get_constraints()
-                cons.insert(dfs[tr["name"]] == 0)
-                newpoly = C_Polyhedron(cons)
+                cons.append(dfs[tr["name"]] == 0)
+                newpoly = C_Polyhedron(constraints=cons, variables=gvs+tr["local_vars"])
                 if not newpoly.is_empty():
                     tr["polyhedron"] = newpoly
                     no_ranked.append(tr)