All pull requests

Pull requests

• perf: Keep the right-totality result until the system changes

  #722·Po-Chun-Chien opened Nov 11, 2026Collaborator·

  ·

• fix: Keep relational and functional transition systems apart

  #718·Po-Chun-Chien opened Nov 7, 2026Collaborator·2/2·

  ·

• fix: Compute whether a transition system is deterministic

  #717·Po-Chun-Chien opened Nov 7, 2026Collaborator·1/2·

  ·

• ci: Build with Z3

  #715·Po-Chun-Chien opened Nov 7, 2026Collaborator·2/2·

  ·

• fix: Read bit-vector values in every form solvers print

  #714·Po-Chun-Chien opened Nov 7, 2026Collaborator·1/2·

  ·

• fix: Keep IC3SA's model cube when no current-state variable justifies it

  #713·Po-Chun-Chien opened Nov 7, 2026Collaborator·

  ·

• fix: Merge IC3SA's equivalence classes of equal arrays

  #712·Po-Chun-Chien opened Nov 7, 2026Collaborator·

  ·

• feat: Functionalize relational transition systems

  #711·Po-Chun-Chien opened Nov 6, 2026Collaborator·

  ·

• perf: Reuse the right-totality result while the system stays the same

  #709·Po-Chun-Chien opened Nov 5, 2026Collaborator·

  ·
  2

• feat: Replace floor, div and mod by literals with variables on request

  #705·Po-Chun-Chien opened Nov 4, 2026Collaborator·2/2·

  ·

• fix: Keep IMC invariants free of bad states without a successor

  #703·Po-Chun-Chien opened Nov 4, 2026Collaborator·

  ·

• fix: Encode Btor2 saddo with a conjunction and smulo on sign-extended operands

  #698·JeetuSK0808 opened Oct 31, 2026·

  ·
  1

• fix: Complement the subtrahend in BTOR2 usubo

  #690·vera-rubin opened Oct 14, 2026·

  ·
  1

  2

• MoXI frontend

  #688·Po-Chun-Chien opened Oct 9, 2026Collaborator·

  ·
  2

• fix: Refuse VMT files that fail to parse

  #687·Po-Chun-Chien opened Oct 7, 2026Collaborator·

  ·
  1

• ci: Bump the pre-commit group across 1 directory with 6 updates

  dependenciespre_commit
  #685·dependabot[bot] opened Oct 6, 2026Bot·

  ·

• fix: Give the SyGuS comparison test a mode of its own

  #681·CyanoKobalamyne opened Sep 21, 2026Member·

  ·

• fix: Keep a constraint over inputs off the initial state

  #665·CyanoKobalamyne opened Sep 21, 2026Member·

  ·

• Add optional IC3Bits partial-model predecessor generalization

  #586·zhanghongce opened Aug 19, 2026Contributor·

  ·

• Timed transition systems and timed VMT front-end

  #534·osankur opened May 13, 2026·

  ·

• SystemVerilog frontend

  #533·CyanoKobalamyne opened May 6, 2026Member·

  ·
  1

• Fix(UB): Fix based on sanitize check

  #528·wjrforcyber opened Mar 21, 2026Contributor·

  ·
  1

• Add a transformation to make transition relation right-total

  #521·Po-Chun-Chien opened Jan 30, 2026Collaborator·

  ·
  1

• Enforce use of relation TS when specified

  #520·Po-Chun-Chien opened Jan 30, 2026Collaborator·

  ·
  5

• Support SMV resize and type-conversion operators

  #475·augustomafra opened Sep 28, 2025Contributor·

  ·
  30