[SMT-LIB] Translating SMT-LIB 1.2 Benchmarks into 2.0?

[Morgan Deters]

Hi Tjark,

Yes, CVC3 does this---but not the current release version.  Recent
nightly builds will do what you want:

  http://goedel.cims.nyu.edu/cvc3-builds/

The command line you'll want is something like

  cvc3 +translate -lang smt -output-lang smt2 benchmark.smt

..and this is (roughly) what we've done to translate the SMT-LIB library.

A caveat: a number of conformance issues have been found with the
SMT-LIB (version 2) library, and some of these represent bugs with the
CVC3 translator that haven't yet been resolved.  We're working on
those, and when you see a new SMT-LIB benchmark announcement on this
mailing list, you'll know also that all known outstanding issues with
the CVC3 translator have been fixed.

Morgan


On Wed, Jan 19, 2011 at 10:02 AM, Tjark Weber <tjark.weber at gmx.de> wrote:
> Is there a tool (or tool chain) that can translate SMT-LIB 1.2
> benchmarks into SMT-LIB 2 format?
>
> Kind regards,
> Tjark
>
> _______________________________________________
> SMT-LIB mailing list
> SMT-LIB at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/smt-lib
>
>



-- 
Morgan Deters
mdeters at gmail.com