What's Changed

• Ensuring that STP's Travis scripts match the lingeling test repo by @aytey in #359
• Ensure we're at the correct directory level when running with Travis by @aytey in #360
• Use linebuf by @aytey in #364
• Disable static builds on Travis by @aytey in #368
• Adding an API routine to allow for obtaining a BV as a bit string by @aytey in #358
• Ensuring that all CMake targets are correct to support no-op builds by @aytey in #374
• Importing the latest 'GetGitRevisionDescription' CMake modules from rpavlik/cmake-modules by @aytey in #372
• Initial work on improving scopes such that symbols are correctly removed by @aytey in #367
• Update docs by @aytey in #371
• remove duplicated cmake option by @hailinzeng in #386
• Ensuring that we do not create double frames when creating a new frame (closes #385) by @aytey in #387
• Creating an API to get the value/index size from a 'Type' by @aytey in #391
• Add Homebrew installation instructions by @carlocab in #400
• ToSATAIG::runSolver now returns the value of SATSolver::solve by @aytey in #397
• Cleaner CMS include and better include location by @msoos in #405
• Fix various warning issues by @Shatur in #410
• Beautify CMake messages by @Shatur in #411
• Add BUILD_EXECUTABLES option by @Shatur in #412
• Working towards using GitHub Actions for CI by @aytey in #378
• Let's not use macros instead of "const"-s by @msoos in #406
• Fix bvExtract interface comment by @Shangyint in #415
• Treat warnings as errors by @aytey in #398
• Modernize Boost usage by @Shatur in #418
• Remove parallel flag because does not work on ctest 3.5.1. by @TrevorHansen in #420
• doc: fix typo by @prncoprs in #423
• Remove the unnecessary use of a SCARY iterator that may break on older compilers by @danielschemmel in #431
• Fixed the broken link on SMT-LIBv2 documentation. by @mnswdhw in #436
• Correcting command line argument for '--max_time' by @aytey in #373
• Rewrite Dockerfile by @rgov in #439
• Fix compilation error on libstdc++-7-dev by @misonijnik in #447
• [gcc 13] include cstdint for int_t by @jirislaby in #462
• Improved let 388 by @TrevorHansen in #469
• Remove nonsensical sbrk usage by @brooksdavis in #474
• Update README.markdown by @TrevorHansen in #442
• Update index.rst by @TrevorHansen in #440
• Get clang building the api tests by @TrevorHansen in #477
• Partially fix Appveyor (windows) automated build. by @TrevorHansen in #478
• Install cadiback dependency by @gussmith23 in #482

New Contributors

• @hailinzeng made their first contribution in #386
• @carlocab made their first contribution in #400
• @Shatur made their first contribution in #410
• @Shangyint made their first contribution in #415
• @prncoprs made their first contribution in #423
• @danielschemmel made their first contribution in #431
• @mnswdhw made their first contribution in #436
• @rgov made their first contribution in #439
• @misonijnik made their first contribution in #447
• @brooksdavis made their first contribution in #474
• @gussmith23 made their first contribution in #482

Full Changelog: smtcomp2020...2.3.4_cadical

STP with CMS and MergeSAT submitted to SMTCOMP 2020.

Windows build finally works without any hitch. So does Linux. This now allows us to create binaries for all platforms.

Fixing displayed version. Python interface updates and a few fixes thanks to all the collaborators and some great merge requests :)

Some ARM compilation fixups

New release of STP to commemorate getting 2nd place in the SMT competition of 2016 bitvector category! Features:

• Fixed divide-by-zero crashes. Divide by zero now defaults to -1
• Uses newest CryptoMiniSat 5.0.0
• Fixed some issues with the python interface
• Fixed some issues with parsing SMT files

Fixing issues with KLEE integration.

Changes

Thanks to Marko Dimjašević a lot of copyright, licensing and author issues have been fixed. This will allow for easier packaging of the STP library and binary into distributions.

High level changes

• Removal of the unmaintained Cryptominisat2
• Addition of Cryptominisat4 at a new SAT solver backend
• minisat is now an external dependency and is no longer bundled in STP.
• Python interface
• Shared library support
• Asserts on by default
• Better build system with automated testing
• Code refactoring

API changes

FatalError callback will assert fail in case the called function returns.