Boolector Release 3.0.0 (MIT license) and Boolector on GitHub

[Aina Niemetz]

Boolector is now hosted on GitHub at https://github.com/boolector/boolector  and licensed under the MIT license.

The Boolector website moved to https://boolector.github.io.

From now on, please prefer the Boolector issue tracker over this google group for bug reports. 

For questions, comments or information on Boolector, please continue posting to this group.

There is a new version (3.0.0) of Boolector available at:

Boolector 3.0.0

Changelog (since version 2.4.1):

• new build system, requires cmake >= 2.8
• setup-*.sh scripts for dependencies (btor2parser, SAT solvers) in contrib
• support for quantified bit-vectors (BV)
• new bounded model checker BtorMC [1]
  
• support for new format BTOR2 [1]
  
• support for CaDiCaL [2] as SAT back-end
  
• SMT2 support for:
  
• echo
• declare-const
• check-sat-assuming
• get-unsat-assumptions
• set-option :produce-unsat-assumptions
• set-option :produce-assertions
• set-logic ALL
• new API calls
  
• boolector_constd
• boolector_consth
• boolector_copyright
• boolector_exists
• boolector_forall
• boolector_get_failed_assumptions
• boolector_repeat
• boolector_pop
• boolector_push
• boolector_version
• removed obsolete API calls:
  
• boolector_set_sat_solver_lingeling
• boolector_set_sat_solver_minisat
• boolector_set_sat_solver_picosat
• changes in API calls:
  
• boolector_srl, boolector_sll and boolector_sra now supports operands with the same bit-width (SMT-LIB v2 compatible)
• various improvements and extensions of BtorMBT

[1] A. Niemetz, M. Preiner, C. Wolf and A. Biere. Btor2, BtorMC and Boolector 3.0. CAV 2018, to appear.

[2] https://github.com/arminbiere/cadical



The documentation of Boolector and it's public APIs can be found at:

https://boolector.github.io/docs/index.html