Requires clauses for tuple-type symbolics not encoded properly
DKLoehr opened this issue · 0 comments
DKLoehr commented
When we have a requires clause for a pair-type symbolic that involves constraints on both elements, only the constraints on the first element are added to the smt encoding. I've pushed a minimal counterexample to examples/debugging.