Once the package loads and CI runs its tests (fix PR: fix/math-swap-and-runtest-pin), the suite reports 818 pass, 6 fail, 6 error on Julia 1.12.6, measured locally with Pkg.test(). These failures were hidden until now: the module failed to parse (math.jl:42), and the julia-runtest pin resolved to no commit, so the test (*) jobs died at setup.
Failures
| Testset |
Location |
What it reports |
| Statistics Parsing / Parse numeric statistics |
test/runtests.jl:876–881 |
get_statistics on "(:time 0.01 :memory 12.5 :conflicts 0)" returns no time, memory or conflicts key (3 fail + 3 KeyError) |
| evaluate / Boolean logic |
test/runtests.jl:931–932 |
evaluate(model, :(p && q)) and :(p || q) give the wrong values |
| Unsat core extraction (Z3) |
test/runtests.jl:1153 |
get_unsat_core returns an empty core for named (x > 0) / (x < 0) assertions with :produce_unsat_cores on. Runs only when z3 is on PATH |
| e2e: declare → assert → check_sat; to_smtlib_script |
test/e2e_test.jl:23, :41 |
UndefVarError: declare_const not defined |
| property: assert! count invariant |
test/property_test.jl:31 |
UndefVarError: declare_const not defined |
Acceptance criteria
Once the package loads and CI runs its tests (fix PR:
fix/math-swap-and-runtest-pin), the suite reports 818 pass, 6 fail, 6 error on Julia 1.12.6, measured locally withPkg.test(). These failures were hidden until now: the module failed to parse (math.jl:42), and thejulia-runtestpin resolved to no commit, so thetest (*)jobs died at setup.Failures
get_statisticson"(:time 0.01 :memory 12.5 :conflicts 0)"returns notime,memoryorconflictskey (3 fail + 3KeyError)evaluate(model, :(p && q))and:(p || q)give the wrong valuesget_unsat_corereturns an empty core for named(x > 0)/(x < 0)assertions with:produce_unsat_coreson. Runs only whenz3is onPATHUndefVarError: declare_const not definedUndefVarError: declare_const not definedAcceptance criteria
get_statisticsparses SMT-LIB(:key value …)statistics into aDict{String,Any}with numeric values, and the four@tests at runtests.jl:876–881 pass.evaluatehandles&&and||(these areExpr(:&&)/Expr(:||), not calls), and runtests.jl:931–932 pass.get_unsat_corereturns the named labels from Z3, or the test states why an empty core is acceptable.declare_constis either added and exported, or the e2e/property tests calldeclare, which is the exported API. Decide which is the intended public surface.Pkg.test()passes on the CI matrix (1.10, 1.11, nightly × ubuntu/macos/windows).