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...

Pono 2.0.0 Beta 1

First beta release for Pono 2.0.

What's Changed

• 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
  ...

HWMCC’25

Version submitted to the 2025 Hardware Model Checking Competition.

HWMCC’24

Version submitted to the 2024 Hardware Model Checking Competition.

Pono 1.0.0

Initial stable Pono version.

Published in:

Mann, M., Irfan, A., Lonsing, F., Yang, Y., Zhang, H., Brown, K., Gupta, A., & Barrett, C. (2021).
Pono: A Flexible and Extensible SMT-Based Model Checker.
In: Silva, A., Leino, K.R.M. (eds) Computer Aided Verification. CAV 2021.
https://doi.org/10.1007/978-3-030-81688-9_22

What's Changed

• Add IC3 via Implicit Predicate Abstraction (IC3IA) by @makaimann in #109
• Refactor Cone Of Influence analysis into a class by @makaimann in #116
• Add smt-switch to install_requires by @makaimann in #118
• Several fixes in IC3IA by @makaimann in #119
• Add a method for replacing terms in the transition relation by @makaimann in #120
• Support to_remove terms directly in ConeOfInfluence reduction by @makaimann in #121
• ic3ia -- Reduce predicates by @ahmed-irfan in #124
• Refactor so Prover has a pointer to the transition system by @makaimann in #125
• change initialize pattern in engines by @ahmed-irfan in #126
• Add cvc4 option to --smt-solver by @makaimann in #127
• Build fixes for --with-msat by @makaimann in #128
• Fix link order between gmpxx and gmp by @makaimann in #129
• Refactor tests to avoid code duplication by @makaimann in #134
• Refactor IC3 implementations to common, parameterized structure by @makaimann in #122
• Updates to install documentation by @makaimann in #130
• Update for smt-switch removal of Iff -- use Equal instead by @makaimann in #137
• Use sequence interpolants in ic3ia refinement by @makaimann in #138
• Functional unroller implementation by @makaimann in #135
• Move COI analysis to main by @makaimann in #139
• Add subterm collector by @makaimann in #136
• adds is_blocked method by @ahmed-irfan in #143
• bugfix in an assertion: rel_ind_check by @ahmed-irfan in #148
• Add reset solver feature to IC3Base by @makaimann in #142
• Ic3 subsumption check by @ahmed-irfan in #146
• ic3* code -- minor changes by @ahmed-irfan in #147
• Minor fix for msat-ic3ia backend by @makaimann in #149
• Create method is_predicate by @makaimann in #152
• Output number of initial predicates with logger by @makaimann in #151
• Fix warning about FunctionalUnroller::at_time not marked override by @makaimann in #153
• const ts in prop constructor by @ahmed-irfan in #155
• simplify prover interface by @ahmed-irfan in #154
• Make KInduction destructor virtual because it's a parent class by @makaimann in #157
• Separate COI analysis from TS transformation by @makaimann in #158
• Use priority queue to manage proof goals by @makaimann in #156
• Add option to replace init and prop with fresh state variables by @makaimann in #160
• const orig ts by @ahmed-irfan in #162
• Use unique term id to sort by @makaimann in #161
• Cython pointer cleanup by @makaimann in #115
• Prover update 2 by @ahmed-irfan in #164
• Prover update 3: adds Engine enum to Pover by @ahmed-irfan in #165
• Fixes for msat-ic3ia after prover-update by @makaimann in #168
• Prover update 4: unifies the engines interface by @ahmed-irfan in #167
• cegar and cegar-proph template by @ahmed-irfan in #170
• Set solver options and refactor smt solver related code by @makaimann in #169
• Update unroller by @ahmed-irfan in #171
• Refactor proof queue by @makaimann in #174
• Additional options for get_predicates by @makaimann in #172
• Refactor inductive generalization by @makaimann in #175
• simplify unroller interface by @ahmed-irfan in #176
• Refactor and add assertions in ic3ia for reduce_predicates by @makaimann in #178
• various: initialize in axiom-enumerator, abstractor: make do_abstraction public, update unroller, update ceg-proph code by @ahmed-irfan in #173
• Improvements and default implementation of inductive_generalization by @makaimann in #177
• Transfer property as BOOL -- helps for sort aliasing solvers by @makaimann in #180
• Keep state variables occurring in INIT in COI analysis by @makaimann in #179
• IC3Base: Use rel_ind_check in propagate and find_highest_frame by @makaimann in #181
• initialize-pattern fixes by @ahmed-irfan in #182
• minor: reset solver after each propagate phase by @makaimann in #184
• IC3IA: do a single iteration of reduction in reduce_predicates by @makaimann in #185
• Change implicit abstraction class by @ahmed-irfan in #188
• Various minor fixes by @makaimann in #190
• Incremental ceg-prophecy by @ahmed-irfan in #187
• Improved IC3IA options by @makaimann in #192
• Add an option to assume the property in the pre-state by @makaimann in #193
• Strengthen prop in IC3 variants by @makaimann in #194
• Temporary configuration fix for CegProphecyArrays by @makaimann in #197
• add array integer and fix some bugs for modular smv by @yangy96 in #189
• A few SMV fixes by @makaimann in #198
• Fixes mismatched push/pop in encoder and sets solver options up front by @makaimann in #199
• CEGAR loop to abstract values by @makaimann in #196
• Fix: move refinement so that one-step CEXs are refined by @makaimann in #200
• Do not increment i after refinement by @makaimann in #203
• Add property in get_frame_term by @makaimann in #202
• refactor array abstactor modifier by @ahmed-irfan in #205
• Minor: Don't re-add property to invariant frame by @makaimann in #206
• Fix push/pop mismatch in array_axioms_refiner by @makaimann in #201
• Create option for cutoff value of CegarValues by @makaimann in #208
• Ic3ia: exclude unused symbols from cubes by @makaimann in #209
• Use witness length when refining in CegProphecyArrays by @makaimann in #211
• De-duplicate the options code in main by @makaimann in #213
• Disable witness generation/printing by default by @makaimann in #210
• Minor fix to comments in IC3Base::reaches_bad by @makaimann in #215
• Add option to promote input variables to state variables by @makaimann in #214
• Relational pseudo init and property transformation by @makaimann in #212
• Declare ProofGoalQueue in header by @makaimann in #216
• Turn off assume-prop in pre-state by default by @makaimann in #219
• IC3Base: Add option to disable unsat core generalization by @makaimann in #217
• St...

Pono 0.1.1

Full Changelog: v0.1.0...v0.1.1

Pono 0.1.0

First release

What's Changed

• All changes for HWMCC19 and subsequent fixes by @makaimann in #3
• Minor changes to reflect smt-switch API changes by @makaimann in #4
• unroller fix and cleaning by @ahmed-irfan in #6
• Engines cleanup by @ahmed-irfan in #5
• Update the clang format style by @makaimann in #7
• Make building with mathsat optional by @makaimann in #9
• License by @ahmed-irfan in #8
• Assert size of states by @makaimann in #10
• Build cosa2 library along with binary by @makaimann in #11
• Fixes to Transition Systems by @makaimann in #17
• minor const fixes by @ahmed-irfan in #23
• Adds instructions for generating BTOR2 to README by @makaimann in #25
• VCD Trace Dump by @zhanghongce in #28
• smv frontends by @yangy96 in #19
• Make sure terms_ is set in every path of parse in btor2encoder except for sorts by @makaimann in #34
• Add python bindings for cosa2 by @makaimann in #24
• Updates to keep in line with smt-switch by @makaimann in #37
• less untime cache by @ahmed-irfan in #42
• Only keep variables as keys in the unroller cache by @makaimann in #41
• CoreIR Encoder by @makaimann in #33
• API Update. Rename: inputs->inputvars, states->statevars by @makaimann in #45
• Set c++17 flags correctly for different versions of CMake by @makaimann in #47
• Rename to pono by @makaimann in #49
• add option to suppress witness printing by @lonsing in #50
• Scanner fixes by @yangy96 in #39
• mc-interp: refactor by @ahmed-irfan in #53
• Handle command line options in a separate PonoOptions class by @lonsing in #51
• Keep track of constraints added to trans through add_constraints, add_invar, and constrain_inputs by @makaimann in #56
• Allow passing Module directly to CoreIREncoder by @makaimann in #58
• Expose the constraints from a TS through the python API by @makaimann in #59
• Add flag to force abstract clock in CoreIR encoding by @makaimann in #60
• Support an install target through cmake by @makaimann in #40
• Interpolant return result by @makaimann in #62
• Fix warning when not built with CoreIR by @makaimann in #61
• Remove dead code from main for option parsing by @makaimann in #63
• Allow using a fresh solver in each engine by @makaimann in #54
• Handle neq for arrays in btor2 encoder by @makaimann in #65
• Add clock and reset options by @makaimann in #70
• Add support for ~rst syntax for negative resets by @makaimann in #72
• Fix in transition system copy constructor by @lonsing in #74
• Fix: Use a disjunction of bad formulas in interp by @makaimann in #76
• Fix copy-paste error in multiply overflow encoding in BTOR2 by @makaimann in #80
• Fix copy paste error in uaddo encoding by @makaimann in #81
• Static cone-of-influence analysis by @lonsing in #75
• Basic IC3 Implementation by @makaimann in #57
• WIP: CEG-Prophecy implementation in Pono by @makaimann in #69
• Bug fixes for HWMCC2020 by @ahmed-irfan in #82
• Build flex by @makaimann in #84
• VCD Printer Update by @zhanghongce in #85
• Add method to get a name for a term and use it for printing property by @makaimann in #71
• Fix bison library CMAKE lookup by @makaimann in #90
• initial change for modular smv by @yangy96 in #48
• Update smt-switch version by @makaimann in #91
• Use updated CMake files for finding GMP and building Cython bindings by @makaimann in #93
• Add build, deps, pycache dirs to .gitignore by @leonardt in #95
• Fix test path to be relative to file by @leonardt in #97
• Add support for compiling with external coreir by @leonardt in #96
• Check that list of files is nonempty and fix assertion typo in Python coreir encoding test by @makaimann in #99
• Update smt switch and remove *_LOGGING enums for latest version by @makaimann in #100
• Fix for TS copy assignment and a test for it by @makaimann in #88
• Add optional profiling via gperftools by @lonsing in #94
• Expose history modifier in python bindings + make_term fix by @makaimann in #101
• Increment reached_k_ before returning false in InterpolantMC by @makaimann in #102
• [coreir-extern] use /usr install prefix on linux by @leonardt in #103
• Minor fixes for building with CoreIR by @makaimann in #106
• Ic3 refactor by @makaimann in #107
• Introduce monitor state when creating a property by @makaimann in #104
• Use SOURCES variable in cmake instead of target_sources by @makaimann in #111
• Add msat ic3ia backend by @makaimann in #108
• change cexgen option name to pregen by @ahmed-irfan in #112
• Fix in IC3 relational preimage generalization by @makaimann in #113
• Expose VCDWitnessPrinter in Python bindings by @makaimann in #114
• Fixes for automatic PyPi release by @makaimann in #117

New Contributors

• @leonardt made their first contribution in #95

Full Changelog: https://github.com/stanford-centaur/pono/commits/v0.1.0