Pono 2.0.0

Second major release of Pono.

What's changed since Pono 1.0.0

• Liveness support for BTOR2 input — both liveness-to-safety (L2S) and k-liveness algorithms are supported,
• Support for VMT-LIB input,
• New optimization flags for BMC, k-induction, and interpolation-based model checking (IMC),
• Support for interpolation sequence-based model checking (ISMC) and dual approximated reachability (DAR),
• Array support in IC3SA,
• Finite index support in counterexample-guided array prophecy (CEGP),
• Witness generation now supports all engines,
• CEGAR for arithmetic operations now supports most engines and can be configured to use free variables instead of UFs,
• Main SMT solver and interpolator and their options can be configured individually.

For details, see our FM 2026 paper "Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness" and its reproduction package at https://doi.org/10.5281/zenodo.18680797.

Merged pull requests

• SyGuS-PDR Bug Fix by @zhanghongce in #243
• SyGuS-PDR option by @zhanghongce in #244
• IC3SA: traverse formula iteratively as DAG in justify_coi by @makaimann in #245
• Ceg proph uf abs by @ahmed-irfan in #246
• Mark witness_length as overridden by @makaimann in #247
• Add test for modifiers in python interface by @makaimann in #248
• Switch CI to GitHub Actions by @makaimann in #251
• Remove unused ic3_reset_interval option by @makaimann in #252
• Allow quoted symbol names in SMV by @makaimann in #253
• Various fixes for using Pono as a library or through Python by @makaimann in #255
• Cegp fixes by @makaimann in #254
• Don't break early if searching subterms in get_predicates by @makaimann in #260
• Automatically promote input variables in BTOR2 constraints by @makaimann in #261
• Keep reference to TS in encoders at python level by @makaimann in #264
• Update smt switch version by @makaimann in #265
• Switch back to FindPythonInterp for now by @makaimann in #267
• Add UF support to SMV frontend by @makaimann in #263
• Align reached_k by @makaimann in #269
• Disable support for finite domain indices in CEGP by @makaimann in #271
• Add option to CEGP to force underlying engine to restart after refinement by @makaimann in #272
• Throw exception if attempting to use cvc4 with a multi-solver engine by @makaimann in #274
• Various Python bindings features by @makaimann in #266
• Update Smt-Switch by @makaimann in #275
• Minor fix in CEGP index check code by @makaimann in #276
• Expose unroller time ID in Python API by @makaimann in #277
• Add IC3Bits and IC3SA to Python API by @makaimann in #278
• Cleanup in repository by @makaimann in #279
• Update smt-switch by @makaimann in #280
• Add option to disable reducing predicates in ic3ia by @makaimann in #281
• Do a single iteration when reducing predicates in ic3ia by @makaimann in #282
• Fix edge case in logger string formatting by @makaimann in #285
• Stream printing for ProverResult and engines by @makaimann in #283
• Fix non-consecutive axiom reduction in CEGP by @makaimann in #284
• Add strong abstraction option for CEGP-arrays by @makaimann in #286
• Fix BMC/K-Induction printing for repeated check_until calls by @makaimann in #287
• Improvements to CEGP by @makaimann in #289
• Add VMT frontend by @makaimann in #288
• Options to disable important vars and distinguish types of axiom redu… by @makaimann in #290
• CEGP: Fixes for indices with next vars in them by @makaimann in #291
• IC3IA: Continue even if predicate reduction fails by @makaimann in #292
• Enable witness printing when using static COI by @lonsing in #293
• Update python-api simple_alu.py example by @makaimann in #294
• Explicitly find python library by @makaimann in #295
• Time stamping by @lonsing in #296
• tests/CMakeLists.txt.in: the default branch of google/googletest is 'main' by @umarcor in #297
• Update CI workflow: build CVC4 from scratch rather than download by @lonsing in #299
• update smt-switch-version by @lonsing in #300
• Fix: CI flow on MacOS by @lonsing in #302
• BMC options for improved bug hunting by @lonsing in #301
• BMC option: allow non-minimal cex by @lonsing in #303
• BMC: fix printing by @lonsing in #304
• K-induction refactoring by @lonsing in #305
• Fix installation of IC3ia and update MathSAT by @lonsing in #306
• Fix CoreIR installation by @lonsing in #308
• Update to use cvc5 by @lonsing in #307
• Allow using cvc5 in IC3 variants by @lonsing in #310
• K-induction: one-time base case check and interval unrolling by @lonsing in #312
• README update by @lonsing in #311
• Update smt switch by @ahmed-irfan in #314
• Create virtual environment for Python packages in CI by @CyanoKobalamyne in #325
• Update smt-switch to pull in bitwuzla fixes by @CyanoKobalamyne in #324
• Add errexit bash option to setup scripts by @CyanoKobalamyne in #323
• Allow using local GTest by @CyanoKobalamyne in #328
• Update Github links by @CyanoKobalamyne in #329
• Update btor2tools version built by contrib script by @CyanoKobalamyne in #330
• Add missing Python dependency to CI by @CyanoKobalamyne in #326
• Update setuptools by @CyanoKobalamyne in #331
• Enable IC3SA for arrays by @CyanoKobalamyne in #332
• Remove unneeded librt causing issues during static compilation by @CyanoKobalamyne in #333
• Use smt-switch version patched with fixes for static compilation by @CyanoKobalamyne in #334
• Add support for bitwuzla in pono binary by @CyanoKobalamyne in #335
• Update Bison to fix Clang error by @CyanoKobalamyne in #337
• Update btor2tools by @CyanoKobalamyne in #338
• Update smt-switch to July 18 version by @CyanoKobalamyne in #336
• Exclude MathSAT from CI runs on macOS by @CyanoKobalamyne in #339
• Do not limit depth when cloning btor2tools by @CyanoKobalamyne in #340
• Exclude state variables without update functions in simple path check by @CyanoKobalamyne in #341
• Add option to create printing solver by @CyanoKobalamyne in #343
• Update smt-switch version by @CyanoKobalamyne in #344
• Fix CI deps for Bitwuzla installation by @CyanoKobalamyne in #347
• Switch default solver to Bitwuzla by @CyanoKobalamyne in #348
• Fix naming of automatically generated next-state variables by @CyanoKobalamyne in #349
• Don't exit MathSAT setup script halfway through by @CyanoKobalamyne in #351
• Enable Yices2 backend by @CyanoKobalamyne in #350
• Throw exception when IC3 bad state reachability check result is unknown by @CyanoKobalamyne in #352
• Remove unneeded boolector include by @CyanoKobalamyne in #353
• Change minimum CMake version to 3.5 by @CyanoKobalamyne in #354
• Revert "Change minimum CMake version to 3.5" by @CyanoKobalamyne in #355
• Adjust bound and witness when monitor state is added to TS by @CyanoKobalamyne in #356
• Fix typo in warning message by @CyanoKobalamyne in #359
• Use next-state suffix when promoting input vars by @CyanoKobalamyne in #360
• Format solver enums by @CyanoKobalamyne in #362
• Only print COI traversal for verbosity >=4 by @CyanoKobalamyne in #363
• Make make install less verbose by @CyanoKobalamyne in #364
• Do not build tests for make all or make install by @CyanoKobalamyne in #365
• Ignore gdb history files by @CyanoKobalamyne in #366
• Move asserts inside conditional by @CyanoKobalamyne in #367
• Fix printing solver creation for MathSAT by @CyanoKobalamyne in #368
• Update IC3ia to version 23.05 by @Po-Chun-Chien in #375
• Fix code style by @CyanoKobalamyne in #374
• Add an option "--version" to print version and exit by @Po-Chun-Chien in #372
• Promote inputs in Btor2's bad to states by @Po-Chun-Chien in #379
• Point btor2tools setup script to commit with CMake fix by @CyanoKobalamyne in #383
• Adhere to project's clang-format setting by @Po-Chun-Chien in #386
• fix warning in op-abstractor by @ahmed-irfan in #387
• Only trigger CI on push by @CyanoKobalamyne in #388
• Bump minimum CMake version to 3.5 by @CyanoKobalamyne in #382
• Check if user-specified bound is valid by @Po-Chun-Chien in #378
• Enable cvc5's interpolation by @Po-Chun-Chien in #385
• Configurable smt-switch directory by @CyanoKobalamyne in #327
• Fix static builds by @CyanoKobalamyne in #390
• Refactor: local variables in a function should not be class members by @CyanoKobalamyne in #393
• Print installed solvers during smt-switch setup by @Po-Chun-Chien in #392
• Add Dockerfile for building container image by @Po-Chun-Chien in #391
• Add git metadata to container image's label by @Po-Chun-Chien in #394
• Rename Btor2 symbols internally by @Po-Chun-Chien in #384
• Add missing header by @CyanoKobalamyne in #397
• Don't install already installed packages in macOS CI by @CyanoKobalamyne in #398
• Store failing test log in CI by @Po-Chun-Chien in #396
• Clean up preprocessor directives and try-catch related to MathSAT by @Po-Chun-Chien in #395
• Run all build strategies completely even if one fail by @Po-Chun-Chien in #401
• Assign unique artifact name to each job by @Po-Chun-Chien in #407
• Fix and modernize Python package setup by @CyanoKobalamyne in #409
• Remove unneeded deps from CI by @CyanoKobalamyne in #410
• Update to stanford-centaur/smt-switch@80ff751 by @CyanoKobalamyne in #411
• Liveness property support by @CyanoKobalamyne in #389
• Add python3-pip and python3-venv to docker build by @CyanoKobalamyne in #412
• Cast init term to bit-vector by @Po-Chun-Chien in #399
• Add clangd configuration file by @CyanoKobalamyne in #416
• Create separate safety and liveness property classes by @CyanoKobalamyne in #415
• New options and improvements to interpolation-based engine by @Po-Chun-Chien in #381
• Do no simulate abstract CEX during IC3IA's refinement, perform BMC instead by @Po-Chun-Chien in #414
• Add documentation for property classes by @Po-Chun-Chien in #425
• Add an option to dump Btor2 witness to file by @Po-Chun-Chien in #373
• Correctly pass options into interp parameterized tests by @Po-Chun-Chien in #427
• Refactor(UnsignedConvert): atoi to stoul by @wjrforcyber in #406
• Convert size_t options to unsigned long by @CyanoKobalamyne in #424
• Add docs build target by @CyanoKobalamyne in #420
• Create BaseProver and SafetyProver classes by @CyanoKobalamyne in #418
• Export violation witnesses for IC3 engines by @Po-Chun-Chien in #421
• Test generation of violation witnesses by @Po-Chun-Chien in #422
• Extend BV arith CEGAR to support more backend engines by @Po-Chun-Chien in #426
• Add interpolation-sequence-based model checking algorithm by @Po-Chun-Chien in #400
• Update the name of Boolector build script by @Po-Chun-Chien in #431
• Update to stanford-centaur/smt-switch@85304dd by @CyanoKobalamyne in #430
• Create liveness prover class by @CyanoKobalamyne in #419
• Abstract bit-vector arithmetic using free state symbols by @Po-Chun-Chien in #428
• Disable compute_witness in CEGAR class by @Po-Chun-Chien in #435
• Unroll formulas at step 0 of ISMC by @Po-Chun-Chien in #433
• Log the SMT solver and interpolator being used by @Po-Chun-Chien in #437
• Compute witness from concrete transition relation in IC3IA and IC3SA by @Po-Chun-Chien in #432
• Implement Dual Approximated Reachability by @Po-Chun-Chien in #434
• Store concrete CEX from the failing refinment query of CEGAR BV-arith by @Po-Chun-Chien in #436
• Enable BV index sort in CEGP by @Po-Chun-Chien in #438
• Update to stanford-centaur/smt-switch@d9f898d by @CyanoKobalamyne in #443
• Allow ISMC and DAR run in CEGAR BV arith by @Po-Chun-Chien in #440
• Add tests for CEX computation and the correctness of invariant in Ceg-Ops-Uf engines by @Po-Chun-Chien in #442
• Upload static binary as artifact by @CyanoKobalamyne in #444
• Fix witness export in shortest-CEX search for BMC by @Po-Chun-Chien in #446
• Simplify and reorganize parallel portfolio script by @CyanoKobalamyne in #445
• Remove unused shell scripts by @CyanoKobalamyne in #447
• Point btor2tools back to the official repository by @Po-Chun-Chien in #449
• Update versions of GitHub actions: checkout and upload-artifact by @Po-Chun-Chien in #450
• Update smt-switch to ac27d8c by @CyanoKobalamyne in #448
• k-induction: Fix error when solver returns unknown by @CyanoKobalamyne in #451
• Fix witness syntax for array value assignment by @Po-Chun-Chien in #456
• Print error messages to stderr by @Po-Chun-Chien in #460
• Do not hardcode solver in op abstrator by @Po-Chun-Chien in #459
• parallel portfolio: look in source instead of working dir for binary by @CyanoKobalamyne in #455
• parallel portfolio: remove special handling of smt-solver options by @CyanoKobalamyne in #454
• Update smt-switch to v1.0.0 by @CyanoKobalamyne in #464
• Add optimized builds to CI by @CyanoKobalamyne in #462
• ci: Fix log file names by @CyanoKobalamyne in #468
• Move EXCLUDE_FROM_ALL from individual test targets to test subdir by @CyanoKobalamyne in #466
• parallel portfolio: Better help message by @CyanoKobalamyne in #465
• parallel porfolio: implement Python suggestions from ruff by @CyanoKobalamyne in #453
• Allow users to pass options to SMT solver by @Po-Chun-Chien in #458
• Fix syntax error in parallel_pono.py by @CyanoKobalamyne in #471
• parallel portfolio: Increase default bound by @CyanoKobalamyne in #472
• Build pono with Boolector by @CyanoKobalamyne in #461
• parallel portfolio: Allow specifying pono binary name by @CyanoKobalamyne in #463
• Do not print to standard output in tests by @CyanoKobalamyne in #473
• ic3bits: Remove extraneous info from error message by @CyanoKobalamyne in #478
• Update smt-switch to version 1.0.1 by @CyanoKobalamyne in #479
• Remove bison script by @CyanoKobalamyne in #480
• Update Dockerfile with bison changes by @CyanoKobalamyne in #481
• Fix base case when --kind-one-time-base-check is enabled by @Po-Chun-Chien in #469
• Fix Relational Transition Systems soundness bugs by @augustomafra in #474
• Promote inputs in prop by @Po-Chun-Chien in #476
• Collect interpolation stats in engines interp, ismc, and dar by @Po-Chun-Chien in #477
• Soundly add monitor state by @Po-Chun-Chien in #470
• Fix test headers by @CyanoKobalamyne in #483
• Fixed Yosys manual link in README by @nwad123 in #484
• Run setup-smt-switch.sh through shfmt by @CyanoKobalamyne in #485
• Update MathSAT to 5.6.12 by @CyanoKobalamyne in #467
• Enable support for Z3 by @CyanoKobalamyne in #486
• Export Btor2 violation witnesses for justice by @Po-Chun-Chien in #488
• Implement k-liveness by @Po-Chun-Chien in #482
• Fix default interpolator enum by @CyanoKobalamyne in #489
• Update smt-switch to v1.0.2 by @CyanoKobalamyne in #491
• Add missing package for envsubst by @CyanoKobalamyne in #492
• Fix interpolator engine tests by @CyanoKobalamyne in #490
• Remove special cases for MathSAT by @CyanoKobalamyne in #493
• Skip creating lambda indices in array axiom enumerator by @CyanoKobalamyne in #494
• Enable counterexample-guided prophecy for all solvers by @CyanoKobalamyne in #495
• Update smt-switch to 1.0.3 by @CyanoKobalamyne in #496
• Fix Python tests for Yices2 and Z3 by @CyanoKobalamyne in #497
• ci: Run only static builds by @CyanoKobalamyne in #498
• Add printing interpolator option by @CyanoKobalamyne in #499
• Use system Btor2tools if available by @CyanoKobalamyne in #505
• Use find_package instead of pkg-config for Z3 by @CyanoKobalamyne in #506
• Improve smt-switch setup script by @CyanoKobalamyne in #507
• Update Smt-Switch to 1.0.6 by @CyanoKobalamyne in #508
• Remove flex setup script by @CyanoKobalamyne in #509
• Run Docker build in PRs; push images only on main by @Po-Chun-Chien in #511
• Remove flex script command from Dockerfile by @CyanoKobalamyne in #512
• Fix setup-smt-switch.sh on Bash 3.2 by @CyanoKobalamyne in #514
• Perform COI-based simplification before L2S by @Po-Chun-Chien in #515
• Avoid excessive use of reset-assertions in interpolation-based engines by @Po-Chun-Chien in #510
• Fix namespace in utils/container_shortcuts.h by @CyanoKobalamyne in #503
• Remove unnecessary destructors by @CyanoKobalamyne in #500
• Fix functions that don't return on all paths by @CyanoKobalamyne in #502
• Make engine_ field constant and pass it through constructors by @CyanoKobalamyne in #501
• Fix boolean printing for VCD by @CyanoKobalamyne in #516
• Add missing case in to_string by @CyanoKobalamyne in #517
• Fix CEX when --pseudo-init-prop is enabled by @Po-Chun-Chien in #519
• Move 'no-' to the beginning of options by @CyanoKobalamyne in #518
• Format CMakeLists.txt files with gersemi by @CyanoKobalamyne in #522
• Remove linking with liby by @CyanoKobalamyne in #524
• Update smt-switch to 1.1.1 by @CyanoKobalamyne in #525
• Remember starting solver context level in provers by @CyanoKobalamyne in #529
• Run tests with all available interpolators by @CyanoKobalamyne in #530
• Enable Bitwuzla's interpolation by @Po-Chun-Chien in #439
• Update smt-switch to 1.1.3 by @CyanoKobalamyne in #531

New contributors

• @umarcor made their first contribution in #297
• @CyanoKobalamyne made their first contribution in #325
• @Po-Chun-Chien made their first contribution in #375
• @wjrforcyber made their first contribution in #406
• @augustomafra made their first contribution in #474
• @nwad123 made their first contribution in #484

Full changelog: v1.0.0...v2.0.0