Discrepancy in symbolics between interpreter and native simulator

[nickgian]

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]

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]

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]

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