-
Notifications
You must be signed in to change notification settings - Fork 0
Issues
is:issue state:open
is:issue state:open
Issue creation is restricted in this repository
Search results
QF_BV theory too narrow for real benchmarks (needs extract/concat, ite-over-BV, sound unsigned, multi-width)
area:bitvectorQF_BV theoryQF_BV theoryenhancementNew feature or requestNew feature or requestseverity:mediumSignificant smell / missing handlingSignificant smell / missing handlingStatus: Open.QF_UF: arity>0 Bool uninterpreted predicates approximated as independent atoms (drops congruence → potential spurious SAT)
area:parserParsers / lexers / CLIParsers / lexers / CLIseverity:mediumSignificant smell / missing handlingSignificant smell / missing handlingsoundnessCan produce a wrong SAT/UNSAT verdictCan produce a wrong SAT/UNSAT verdictStatus: Open.Lazy SMT loop enumerates all Boolean models (exponential; no DPLL(T) theory propagation)
area:smt-coreLazy SMT loop / SAT-theory interfaceLazy SMT loop / SAT-theory interfaceenhancementNew feature or requestNew feature or requestseverity:mediumSignificant smell / missing handlingSignificant smell / missing handlingStatus: Open.Epic: post-audit remediation — SMT-LIB front-end (all 6 logics) + soundness fixes
infrastructureTooling / validation infrastructureTooling / validation infrastructureStatus: Open.#35 In paultristanwagner/satisfiability-checking;SMT-LIB benchmark loader + :status oracle runner
area:testingTestsTestsinfrastructureTooling / validation infrastructureTooling / validation infrastructureStatus: Open.SMT-LIB 2.6 subset parser (front-end to internal structures)
area:parserParsers / lexers / CLIParsers / lexers / CLIinfrastructureTooling / validation infrastructureTooling / validation infrastructureStatus: Open.Differential testing harness (EnumerationSolver oracle + known-answer cases)
area:testingTestsTestsinfrastructureTooling / validation infrastructureTooling / validation infrastructureStatus: Open.No verdict-level tests for the SMT/theory layer; no malformed-input rejection
area:testingTestsTestsseverity:mediumSignificant smell / missing handlingSignificant smell / missing handlingStatus: Open.assign/propagate polarity asymmetry (fragile; phase logic dead)
area:satSAT core (DPLL/CDCL)SAT core (DPLL/CDCL)severity:lowStyle / minor cleanupStyle / minor cleanupStatus: Open.Build inconsistencies: compiler 13 vs 16, mixed JLine versions, version drift
area:buildBuild / deps / docsBuild / deps / docsseverity:mediumSignificant smell / missing handlingSignificant smell / missing handlingStatus: Open.Hot-path inefficiencies: full-scan BCP, no Clause equality, per-token regex compile
area:satSAT core (DPLL/CDCL)SAT core (DPLL/CDCL)enhancementNew feature or requestNew feature or requestseverity:mediumSignificant smell / missing handlingSignificant smell / missing handlingStatus: Open.Hex bit-vector constant crashes with uncaught UnsupportedOperationException
area:parserParsers / lexers / CLIParsers / lexers / CLIbugSomething isn't workingSomething isn't workingseverity:lowStyle / minor cleanupStyle / minor cleanupStatus: Open.