Requires clauses for tuple-type symbolics not encoded properly

NetworkVerification / nv

A Framework for Modeling and Analyzing Network Configurations

MIT License

31 stars 2 forks source link

Requires clauses for tuple-type symbolics not encoded properly #31

Closed DKLoehr closed 4 years ago

DKLoehr commented 4 years ago

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.