Problem when declaring variables with same name in different scopes (e.g. two if/else branches)

The following code causes issues in the Z3-translator, because the variable light is declared in both* branches. To solve, we have to declare the variable outside.

In fact, the current implementation forbids any two variables with the same name.

@update(state = state, target = light_Out)
def update_light_out(self, dt):
    # FIX: write light = 0 here
    if(self.time_Local.value%1440 > 21*60):
        light = 0
    elif(self.time_Local.value%1440 > 16*60):
        light = 20000*(21*60-self.time_Local.value)//60 #On veut 20000*un nombre flottant entre 0 et 5
    elif(self.time_Local.value%1440 > 12*60):
       light = 100000
    elif(self.time_Local.value%1440 > 7*60):
        light = 20000*(abs(self.time_Local.value - 7*60))//60  #On veut 20000*un nombre flottant entre 0 et 5
    else:
       light = 0

    return light

Solution: The current solution is to declare a variable in an outside scope (e.g. light = 0 on line 3). Thus, the original variable will be reassigned, instead of declared again.

Potential issues: This doesn't work if you want to have the same variable name for values of different type (e.g. one light of type REAL and one of type string).

The AST treats elif ...: as else: if ... :

crestdsl / CREST

Problem when declaring variables with same name in different scopes (e.g. two if/else branches) #21