[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