search

smackers / smack

SMACK Software Verifier and Verification Toolchain
http://smackers.github.io
Other
432 stars 82 forks source link

support for CVC4 #76

Closed pdeligia closed 9 years ago

pdeligia commented 9 years ago

As discussed with Zvonimir already, SMACK generates some variables (for example .str) that begin with ".". When Boogie translates the SMACK code to SMTLIB2 and passes it to CVC4, CVC4 complains that:

(error "Parse Error: test.smt2:26.17: cannot declare or define symbol `.str'; symbols starting with . and @ are reserved in SMT-LIB

(declare-fun .str () Int) ^ ")

The reason is that "." and "@" are reserved in the SMTLIB standard.

It would be nice for SMACK to use another prefix symbol, so it can support CVC4 in the near future.

michael-emmi commented 9 years ago

I wonder whether this should be fixed in Boogie rather than SMACK. Thoughts?

zvonimir commented 9 years ago

My inclination was also that this should be fixed in Boogie. I still wanted that we briefly discuss it.

pdeligia commented 9 years ago

Yea, maybe it makes more sense to fix it inside Boogie. Plus, I believe they have a pass already for changing the @ prefix to "AT", so only the . is giving a problem. I do not have commit rights there, but I will try see if I can get it done at some point.

Also as you know Z3 is now MIT license, so its not so critical to support CVC4 immediately (for industry adoption), but it would be really nice to have both Z3 and CVC4 measurements in future papers, as it makes any claims stronger.

michael-emmi commented 9 years ago

Perhaps we should create a Boogie issue for this?

michael-emmi commented 9 years ago

Decidedly a fix for Boogie.