13 Pull requests merged by 3 people

• Update CVC5 to 1.2.X

  #454 merged Mar 28, 2025

• Extend Mathsat5 Native Wrapper with API for Proofs

  #460 merged Mar 22, 2025

• Add support for integer modulo in MathSAT

  #459 merged Mar 22, 2025

• Add special-case handling for distinct() with fewer than 2 arguments

  #465 merged Mar 22, 2025

• Fix empty sums in Z3

  #464 merged Mar 22, 2025

• Allow empty String ranges

  #456 merged Mar 19, 2025

• Reorder test formula in testStringVariableReplaceSubstring() to fix Z3 regression

  #455 merged Mar 18, 2025

• Fix library symlinks

  #453 merged Mar 17, 2025

• Remove boolector quantifiers standalone

  #449 merged Mar 15, 2025

• Extend mathsat wrapper with more parse functions

  #445 merged Mar 14, 2025

• Tests: replace "@Test(expected = *Exception.class)" with proper "assertThrows(*Exception.class, () -> ...)".

  #452 merged Mar 9, 2025

• FP theory: improve documentation and tests.

  #440 merged Mar 1, 2025

• Tweak TimeoutTest Parameters due to Bitwuzla Windows Flaky Test

  #441 merged Mar 1, 2025

6 Pull requests opened by 5 people

• Extend Docker images and CI

  #442 opened Mar 2, 2025

• Add Proper Yices2 Quantifier Support

  #447 opened Mar 6, 2025

• Develop a common proof format and export proofs

  #458 opened Mar 19, 2025

• Add solver independent quantifier elimination with ultimate eliminator

  #462 opened Mar 20, 2025

• Add explicit cast in mixed integer-real term

  #466 opened Mar 22, 2025

• Add JavaSMT project template for Ivy/Ant

  #467 opened Mar 23, 2025

5 Issues closed by 3 people

• [Feature Request] Support for NetBSD Operating System

  #443 closed Mar 31, 2025

• Update CVC5 to version 1.2.0 or newer

  #410 closed Mar 28, 2025

• Z3: Regression in String theory with update to 4.14.0

  #439 closed Mar 18, 2025

• Suggested improvements for API related to floats

  #433 closed Mar 2, 2025

• Bitwuzla on Windows: Regression with update to 0.7.0-13.1-g595512ae

  #435 closed Mar 1, 2025

8 Issues opened by 4 people

• [CVC5 on Windows] SegFault when creating multiple CVC5 instances

  #469 opened Mar 29, 2025

• Update to SMTInterpol Version 2.5-1388

  #468 opened Mar 27, 2025

• Problems with installation

  #463 opened Mar 21, 2025

• Z3 fails when given mixed integer-real arguments for division

  #461 opened Mar 19, 2025

• Segfault in Z3 when calling IntegeFormulaManager.mkNumber with a BigDecimal value

  #457 opened Mar 18, 2025

• SMTLib2 Output Consistency for Quantified Terms

  #450 opened Mar 7, 2025

• Update to Java 17 for Next Major Release

  #446 opened Mar 4, 2025

• Extend MathSAT5 SMTLib2 Dumping for Quantified Formulas or Disallow Quantifiers

  #444 opened Mar 3, 2025

4 Unresolved conversations

Sometimes conversations happen on old items that aren’t yet closed. Here is a list of all the Issues and Pull Requests with unresolved conversations.

• Extend Solver Independent SMTLib2 Parser/Generator

  #436 commented on Mar 31, 2025 • 26 new comments

• Improve Documentation of Non-Trivial Operations

  #403 commented on Mar 4, 2025 • 0 new comments

• Unwanted output in tests (and probably outside of it, too)

  #392 commented on Mar 7, 2025 • 0 new comments

• Yices2 MacOS Support

  #400 commented on Mar 8, 2025 • 0 new comments