give symbol table quantified variables same unique ID as originator
In this commit we force the synthetic VarDecl in the symbol table that corresponds to a quantified variable to have the same unique identifier as the originating quantifier. Taking a global perspective, I think this is probably a bad idea. This induces multiple differently typed AST nodes with the same unique identifier. Everything matches up conveniently in the SMT bridge, but only sort of coincidentally. A better approach may be to take a step back and construct a VarDecl in a quantifier in the first place.
parent
194f643e
Please register or sign in to comment