SRI-CSL / yices2 / 25524988749

67%

master: 71%

Build Type

Pull #606

github

Committed by disteph

Commit Message

tests: actually exercise ARITH_CEIL dispatch in tuple_unary_arith.ys

The previous header claimed the .ys file covered ARITH_CEIL alongside
ARITH_FLOOR / ARITH_IS_INT_ATOM / ARITH_ABS, but no ceil assertion was
present. The original assumption was that mcsat's nra plugin could not
solve any (= (ceil x) k) constraint and so ceil could only be reviewed
for dispatch by inspection.

That assumption is wrong: mcsat *does* route and answer ceil queries.
Separately, mcsat's nra plugin has a real semantic bug where (ceil x)
is treated like (floor x) for a range of rationals (e.g. it answers
sat for `(ceil 7/2) = 3` and unsat for `(ceil 7/2) = 4`). That bug is
unrelated to the tuple-blast dispatch fix in 9fefa45b and out of scope
for this PR.

So we add a deliberately *lax* ceil constraint over a tuple component
-- (<= (ceil (select x 2)) 100) -- which holds under both the correct
and the buggy interpretation. This exercises the ARITH_CEIL dispatch
arm end-to-end without depending on ceil's exact value, restoring the
header's accuracy. Update the matching note in mcsat_tuples.c to point
at the .ys file's header for the ceil-semantics caveat.

Pull Request Pull Request #606: MCSAT: add support for tuples (incl. nested with function types); blasts tuples in input constraints + reconstitutes them in models and interpolants

Coverage Stats

784 of 1059 new or added lines in 3 files covered. (74.03%)

6 existing lines in 1 file now uncovered.

84648 of 126192 relevant lines covered (67.08%)

1641839.53 hits per line