A timeout is not a pass: “Not determined” results
When the engine runs out of budget or hits a size limit, it reports “Not determined”, never a pass. Below, the normal-form conversion of a 14-input XOR chain stops at the term limit and says so; a check that exceeds its time budget reports the same way.
Every analysis in the engine has a stated limit: truth tables stop at 12 inputs, Karnaugh maps at 4 variables, normal forms at 4,096 terms and 20,000 literal occurrences, the simplifier at 500 steps, and each check and conversion runs under a wall-time budget. When a limit is reached, the result carries a status that says which limit and no verdict at all. The artefact on this page is such a result: the disjunctive normal form of x1 XOR … XOR x14 would have 8,192 terms of 14 literals each, far beyond the limits, and the converter reports that an intermediate expansion exceeded 20,000 literal occurrences, rather than printing a truncated form.
A check behaves the same way. Its verdict is one of three, holds, violated or unknown, and unknown comes with a reason. The user interface shows unknown as “Not determined”, and a stale result, one computed for an earlier revision of the model, is labelled stale. None of these is a pass, and none is a fail; the honest-results rule keeps the transport status (did the computation finish?) separate from the verdict (what did it find?).
The practical consequence for testing is that a suite which treats anything other than “violated” as success will count timeouts as passes. Read the status before the verdict, and when a check is not determined, reduce the model, add assumptions that narrow the scope, or split the rule into named parts the engine can check one at a time.
A result that exceeded the limit
x1 XOR x2 XOR x3 XOR x4 XOR x5 XOR x6 XOR x7 XOR x8 XOR x9 XOR x10 XOR x11 XOR x12 XOR x13 XOR x14
14 inputs · limits: 4096 terms, 20000 literals
Conjunctive normal form (CNF)
Disjunctive normal form (DNF)
The common slip
Writing a CI step that fails only on a counterexample. A check that ran out of budget produced no counterexample and no proof; the CLI reports it as not determined, and the step must treat that as a failure to decide, not as a green light.
Questions
Why not just raise the limits?
Because the honest answer at every size is the same: either the computation finished and the verdict is exact, or it did not and no verdict exists. Limits keep the first case fast and the second case visible; raising them moves the line, it does not remove it.
What does the SMT-LIB export say about unknown?
The same thing: its header states that unknown settles nothing, and that unsat is solver-checked rather than an independently checked proof certificate.
Related
Tools
- Logical equivalence checker: two expressions, exact verdict, counterexample
- Truth table generator: any Boolean expression, up to 12 variables, with intermediate columns
See also
- Coverage is not correctness: tests still need expected results
- Exhaustive check: meaning and examples
- SAT solver: meaning and examples
- Boolean logic in SMT-LIB: declare-const, assert and check-sat with Z3
- CNF and DNF converter: conjunctive and disjunctive normal forms, minterms and maxterms
- A review checklist for decision rules (for analysts and reviewers)
- Distributive law: A AND (B OR C) = (A AND B) OR (A AND C), both forms
Pitfalls
Generated from the Tangibool engine, semantics tangibool-semantics/1, engine 1.0.0, build . Every table, map, simplification and verdict on these pages was computed by the Tangibool engine when the site was built, and every claim was re-checked by the same exact checker the app uses. Limits are stated where they apply. © 2026 Foreranger LTD.