declare Quantifier::decl in the symtab instead of a synthetic VarDecl
We now have references to quantified variables resolving to something non-transient. The motivation for this was to make the SMT bridge's life easier but this actually leads to more overall consistency as well.
parent
4aba73cb
Please register or sign in to comment