fix: declare a quantifier's decl rather than itself in SMT translation
This fixes an issue where malformed SMT problems would be produced from expressions within quantified sections. The quantified variable would be declared using the ID of the quantifier, but then references to it would use the ID of the quantifier's contained declaration. As a result, SMT solvers would reject the problem for referring to an undeclared variable. This bug was actually identified while trying to implement forall support in the SMT bridge. The upcoming tests for this provoke the bug.
parent
37cfa28a
Please register or sign in to comment