All issues

Search results

[soundness] QF_UFIDL: sat on Z3-unsat vhard7.smt2 (SMT-LIB)

Status: Open.

#50 In cool-japan/oxiz;

· 0kenx opened on Aug 8, 2026

[soundness] QF_IDL: sat on Z3-unsat jobshop4-2-2-2-4-4-11 (SMT-LIB)

Status: Open.

#49 In cool-japan/oxiz;

· 0kenx opened on Aug 8, 2026

[soundness] QF_ANIA: sat on Z3-unsat GrandProduct diff/3.smt2 (SMT-LIB)

Status: Open.

#48 In cool-japan/oxiz;

· 0kenx opened on Aug 8, 2026

[soundness] QF_BV: sat on Z3-unsat (bench_679, ext_con_064) (SMT-LIB)

Status: Open.

#47 In cool-japan/oxiz;

· 0kenx opened on Aug 8, 2026

[soundness] QF_UFLIA: sat on Z3-unsat Wisa/wisas (SMT-LIB)

Status: Open.

#46 In cool-japan/oxiz;

· 0kenx opened on Aug 8, 2026

[soundness] QF_LIA: sat on Z3-unsat rings/* (SMT-LIB)

Status: Open.

#45 In cool-japan/oxiz;

· 0kenx opened on Aug 8, 2026

[soundness] QF_AUFLIA: sat on Z3-unsat storecomm/Rodin (SMT-LIB)

Status: Open.

#44 In cool-japan/oxiz;

· 0kenx opened on Aug 8, 2026

[sat] Clause layout: SmallVec<[Lit;4]> spills 5–8 lit clauses; main fits 8 inline in 64B cache line

Status: Open.

#43 In cool-japan/oxiz;

· 0kenx opened on Aug 7, 2026

[sat] Avoid cloning the full trail on every theory-check iteration

Status: Open.

#42 In cool-japan/oxiz;

· 0kenx opened on Aug 7, 2026

[solver] Theory-aware branching: bump finite-domain enumeration atoms

Status: Open.

#41 In cool-japan/oxiz;

· 0kenx opened on Aug 7, 2026

[solver] On model-refutation, block the assignment and continue instead of Unknown

Status: Open.

#40 In cool-japan/oxiz;

· 0kenx opened on Aug 7, 2026

[nia] Simplex-relaxation CDCL(T) engine (nia_cdcl) not ported — noted as future work on #31

Status: Open.

#39 In cool-japan/oxiz;

· 0kenx opened on Aug 7, 2026