diff --git a/stl/stl.g4 b/stl/stl.g4
index 5ab2f23..8a05c5b 100644
--- a/stl/stl.g4
+++ b/stl/stl.g4
@@ -2,8 +2,9 @@ grammar stl;
 
 @header {
 '''
- Copyright (C) 2015-2018 Cristian Ioan Vasile <cvasile@mit.edu>
+ Copyright (C) 2015-2020 Cristian Ioan Vasile <cvasile@lehigh.edu>
  Hybrid and Networked Systems (HyNeSs) Group, BU Robotics Lab, Boston University
+ Explainable Robotics Lab, Lehigh University
  See license.txt file for license information.
 '''
 }
diff --git a/stl/stl.py b/stl/stl.py
index 08f5fbe..7db9084 100644
--- a/stl/stl.py
+++ b/stl/stl.py
@@ -1,6 +1,7 @@
 '''
- Copyright (C) 2015-2018 Cristian Ioan Vasile <cvasile@bu.edu>
+ Copyright (C) 2015-2020 Cristian Ioan Vasile <cvasile@lehigh.edu>
  Hybrid and Networked Systems (HyNeSs) Group, BU Robotics Lab, Boston University
+ Explainable Robotics Lab, Lehigh University
  See license.txt file for license information.
 '''
 
diff --git a/stl/stl2milp.py b/stl/stl2milp.py
index fd30d7f..3db03a6 100644
--- a/stl/stl2milp.py
+++ b/stl/stl2milp.py
@@ -1,6 +1,7 @@
 '''
- Copyright (C) 2018 Cristian Ioan Vasile <cvasile@mit.edu>
+ Copyright (C) 2018-2020 Cristian Ioan Vasile <cvasile@lehigh.edu>
  Hybrid and Networked Systems (HyNeSs) Group, BU Robotics Lab, Boston University
+ Explainable Robotics Lab, Lehigh University
  See license.txt file for license information.
 '''
 
@@ -122,10 +123,9 @@ def disjunction(self, formula, z, t):
     def eventually(self, formula, z, t):
         '''Adds an eventually to the model.'''
         assert formula.op == Operation.EVENT
-        a, b = formula.low, formula.high
+        a, b = int(formula.low), int(formula.high)
         child = formula.child
-        print "a=%d,b=%d"%(a,b)
-        z_children = [self.to_milp(child, t + tau) for tau in range(int(a), int(b+1))]
+        z_children = [self.to_milp(child, t + tau) for tau in range(a, b+1)]
         for z_child in z_children:
             self.model.addConstr(z >= z_child)
         self.model.addConstr(z <= sum(z_children))
@@ -133,11 +133,9 @@ def eventually(self, formula, z, t):
     def globally(self, formula, z, t):
         '''Adds a globally to the model.'''
         assert formula.op == Operation.ALWAYS
-        a, b = formula.low, formula.high
-#        print "a=%d,b=%d,t=%d"%(a,b,t)
+        a, b = int(formula.low), int(formula.high)
         child = formula.child
-        z_children = [self.to_milp(child, t + tau) for tau in range(int(a), int(b+1))]
-#        print len(z_children)
+        z_children = [self.to_milp(child, t + tau) for tau in range(a, b+1)]
         for z_child in z_children:
             self.model.addConstr(z <= z_child)
         self.model.addConstr(z >= 1 - len(z_children) + sum(z_children))
@@ -148,7 +146,7 @@ def until(self, formula, z, t):
 
         raise NotImplementedError #TODO: under construction
 
-        a, b = formula.low, formula.high
+        a, b = int(formula.low), int(formula.high)
         z_children_left = [self.to_milp(formula.left, tau)
                                                  for tau in range(t, t+b+1)]
         z_children_right = [self.to_milp(formula.right, tau)