Severity: Medium · Category: correctness/soundness · Confidence: high (by construction) · Found by: real QF_UF benchmark wiring (PR for define-fun/Bool)
Problem
The SMT-LIB front-end treats an arity>0 Bool-sorted uninterpreted predicate application (e.g. (GrEq_1_32_32 a b)) as an independent propositional atom keyed by its textual form. Two applications with provably-equal arguments are therefore NOT linked: congruence a=a' ∧ b=b' ⇒ f(a,b)=f(a',b') is dropped. This is an over-approximation (admits more models) and can yield a spurious SAT for a formula that is UNSAT only because of predicate congruence.
Evidence / exposure
229 of 304 2018-Goel-hwbench QF_UF benchmarks declare such predicates ((declare-fun GrEq_1_32_32 (utt$32 utt$32) Bool), (declare-fun Add_1_1_1 (Bool Bool) Bool)). Empirically the verdicts were correct on the sampled set (23/25 UNSAT correct, 0 mismatch across ~100 files), so the construct rarely affects the verdict in practice — but soundness is not guaranteed.
Location
parse/SmtLibParser.java (Bool-predicate-application handling).
Fix direction
Either (a) introduce proper EUF congruence for Bool-returning uninterpreted predicates (model (f args) as an EUF term with a Boolean-valued result and add congruence atoms), or (b) add a "strict soundness" mode that rejects arity>0 Bool predicates as unsupported instead of approximating. Until then, QF_UF results on benchmarks using such predicates are best-effort, not guaranteed sound.
Severity: Medium · Category: correctness/soundness · Confidence: high (by construction) · Found by: real QF_UF benchmark wiring (PR for define-fun/Bool)
Problem
The SMT-LIB front-end treats an arity>0 Bool-sorted uninterpreted predicate application (e.g.
(GrEq_1_32_32 a b)) as an independent propositional atom keyed by its textual form. Two applications with provably-equal arguments are therefore NOT linked: congruencea=a' ∧ b=b' ⇒ f(a,b)=f(a',b')is dropped. This is an over-approximation (admits more models) and can yield a spurious SAT for a formula that is UNSAT only because of predicate congruence.Evidence / exposure
229 of 304
2018-Goel-hwbenchQF_UF benchmarks declare such predicates ((declare-fun GrEq_1_32_32 (utt$32 utt$32) Bool),(declare-fun Add_1_1_1 (Bool Bool) Bool)). Empirically the verdicts were correct on the sampled set (23/25 UNSAT correct, 0 mismatch across ~100 files), so the construct rarely affects the verdict in practice — but soundness is not guaranteed.Location
parse/SmtLibParser.java(Bool-predicate-application handling).Fix direction
Either (a) introduce proper EUF congruence for Bool-returning uninterpreted predicates (model
(f args)as an EUF term with a Boolean-valued result and add congruence atoms), or (b) add a "strict soundness" mode that rejects arity>0 Bool predicates as unsupported instead of approximating. Until then, QF_UF results on benchmarks using such predicates are best-effort, not guaranteed sound.