[SMT-LIB] minor updates to benchmarks

Clark Barrett barrett at cs.nyu.edu
Wed Jun 20 11:45:29 EDT 2007


> Hmm.. I had the same problem converting from the Spear format (which also
> allows subexpression sharing) to SMT. The simplest solution is to introduce
> fresh variables. Is there any particular reason why that was infeasible for that
> particular instance?

Not really.  I had a lot of benchmarks to get through and it was just faster
and easier to merge all the assumptions for the stp benchmarks.  I would have
preferred a solution that allows me to introduce global abbreviations (rather
than new variables), so I am going to suggest that goes into the next version
of the SMT-LIB standard.

-Clark


More information about the SMT-LIB mailing list