search

NetworkVerification / nv

A Framework for Modeling and Analyzing Network Configurations
MIT License
31 stars 2 forks source link

Discrepancy in symbolics between interpreter and native simulator #35

Open nickgian opened 4 years ago

nickgian commented 4 years ago

The native simulator ignores values provided for symbolic variables, which causes a different behavior compared to the interpreted simulator. It would be nice to match the two at some point.

alberdingk-thijm commented 4 years ago

Just ran into this issue when running a file through SMT which had the following line:

symbolic dest : tnode = 9n

nv -m -v file.nv returns that dest:0u32.

nickgian commented 4 years ago

That's actually a different issue, it's more of a design choice. In the SMT solver we ignore the rhs value of a symbolic, because the SMT solver can reason about symbolic variables. If the value is supposed to be a constant even for the SMT then use a let declaration instead.

If you really want to keep this as a symbolic, add a requires clause that says dest = 9n.

alberdingk-thijm commented 4 years ago

Gotcha. I changed my code but it would probably be good to mention this in the wiki.