This is the final release of Boolector. Active development and maintenance has
stopped. Boolector was succeeded by Bitwuzla.

• fix issues in btormc
• fix issue with get-value for Boolean variables
• fix issue with get_failed_assumptions in combination with push/pop
• fix get-unsat-assumptions printing
• export enums for setting options (option values)
• get-model is now SMT-LIB standard compliant
• PyPi packages for Boolector
• remove obsolete CL option --smt2-model (use -m --output-format=smt2 instead)

• initial version of Dockerfile for Boolector
  (thanks to Andrew V. Jones)
• fix issue with infinite recursion in Python API
  (thanks to Andrew V. Jones)
• fix issue with dumping constant arrays
• fix issue with reset assumptions and checking of failed assumptions
• fix witness printing in btormc

• new dumper: CNF printer (enable with CLI option -dd and API option BTOR_OPT_PRINT_DIMACS)
• fix issue with model construction for constant arrays
• boolector_sat is not automatically called on smt2 input anymore, must be explicitly called via (check-sat) in the input file
• smt2:
  • support for parsing constant arrays
  • support for :global-declarations
• API changes:
  • boolector_ror and boolector_rol now allow same bit-width for both operands
• new API calls
  • boolector_roli
  • boolector_rori

Changes:

• build system:
  • requires now cmake >= 3.3
  • exports library interface for using find_package(Boolector) in cmake projects
• support for custom abort callback function
  (called on abort instead of actually aborting)
• Python API now throws Python exceptions on abort conditions
  (e.g., when underlying C API is misused)
• command line options that previously expected integer values denoting enum
  values are now configured with strings denoting the particular modes that
  can be selected; -=help and --=help allow to print detailed help
  messages for these modes
• fixed issue in SMT2 parser to correctly print echo commands
  (thanks to Dominik Klumpp)
• fixed race condition in Cython dependencies
  (thanks to Marco Gario)
• patches and documentation for building Boolector on Windows
  (thanks to Andrew V. Jones)
• support/use termination function feature of CaDiCaL
  (thanks to Andrew V. Jones)
• various fixes to contrib dependecy scripts
  (thanks to Serge Bazanski)
• new API calls
  • boolector_copy_sort
  • boolector_min_signed
  • boolector_max_signed
  • boolector_is_bv_const_zero
  • boolector_is_bv_const_one
  • boolector_is_bv_const_ones
  • boolector_is_bv_const_min_signed
  • boolector_is_bv_const_max_signed
• CaDiCaL is now default SAT engine
• support for constant arrays
• support for GMP as bit-vector implementation
• support for CyproMiniSat
  • supports multi-threading via option --sat-engine-n-threads
• switched to Google test as testing framework
• CLI options changed (replaced ':' with a '-')
• BtorMC improvements (HWMCC'19 version)
  • k-induction engine with simple path constraints
• Poolector Python script used in SMT-COMP'19

Changes:

• 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
• support for new format BTOR2
• support for CaDiCaL as SAT back-end
• name of the Python module changed to pyboolector
• 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