search

salmans / Razor

5 stars 0 forks source link

Allow '_0 as a constant #34

Closed ramsdell closed 9 years ago

ramsdell commented 9 years ago

$ cat z.r p('_0); $ razor --input=z.r <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> Input Options: --input=Just "z.r" --debug=False --depth=-1 --command=Nothing --state=Nothing <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><> razor: Bad uninterpreted constant name: "_0". Must be a valid identifier. $

salmans commented 9 years ago

Our old interface library to interact with SMT solvers (SBV) doesn't allow identifiers to begin with "_". We are now using a different SMT library (SMTLib2), which doesn't censor Razor when interacting with the solver but because the new library isn't on Hackage yet, we still use the old library by default. The current fix is an ad-hoc solution to this bug, which may be unstable, but the problem will disappear as soon as we completely switch to the new library (see #21).