Made Preamble more SMTLIBv2 compliant (so that CVC4 understands it).

[viper-admin]

Pull request :twisted_rightwards_arrows: created by bitbucket user snidoom on 2015-09-23 08:09 Last updated on 2015-09-23 08:38 Original Bitbucket pull request id: 18

Participants:

• @mschwerhoff (reviewer)
• bitbucket user snidoom

Source: https://github.com/viperproject/silicon/commit/ac0d1e5882ec2083d588e085b271c367ce211827 on branch snidoom/silicon/smtlib2-compliance Destination: https://github.com/viperproject/silicon/commit/93ea82de1818a6ba57d88d53ae24fb366126ee49 on branch master Marge commit: https://github.com/viperproject/silicon/commit/c2584dfd32ad4b45db9469153c19be23649c7a1c

State: MERGED

Two small changes that allow the preamble.smt2 to be used as is on CVC4 as well as Z3.

[viper-admin]

@mschwerhoff commented on 2015-09-23 08:22

Do you know which Z3 version first supported SMTLib 2.5? Would be interesting for documentation purposes.

[viper-admin]

Bitbucket user snidoom commented on 2015-09-23 08:35

Do you know which Z3 version first supported SMTLib 2.5? Would be interesting for documentation purposes.

From the changelog:

Version 3.0
===========

- Fully compliant SMT-LIB 2.0 (SMT2) front-end. The old front-end is still available (command line option -smtc).
  The <a class="el" href="http://rise4fun.com/z3/tutorial/guide">Z3 Guide</a> describes the new front-end.

It seems that this is the newest SMT-LIB version officially supported. But the features used in this pull request were also present in version 2. I'll edit the title and description.

[viper-admin]

@mschwerhoff commented on 2015-09-23 08:38

No worries, if the changes comply with SMTLIB 2, then we don't need to change any documentation. Thanks!