7 Pull requests merged by 2 people

• 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

5 Pull requests opened by 3 people

• Update CVC5 to 1.2.X

  #454 opened Mar 17, 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

1 Issue closed by 1 person

• Z3: Regression in String theory with update to 4.14.0

  #439 closed Mar 18, 2025

3 Issues opened by 2 people

• 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

1 Unresolved conversation

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 21, 2025 • 0 new comments