signed-subtraction overflow: invalid unsat result

[LeventErkok]

For this benchmark:

(set-logic ALL)
(define-fun s0 () (_ BitVec 3) #b101)
(define-fun s1 () (_ BitVec 3) #b010)
(assert (bvssubo s0 s1))
(check-sat)

z3 says:

unsat

This is incorrect. s0 is -3, s1 is 2, and their difference is -5, which underflows 3-bit signed bit-vector values.

The result should be sat instead.

[LeventErkok]

@aehyvari Based on the commit history, I think you're the right one to look at this..

[LeventErkok]

Hi @aehyvari

Did you get a chance to look at this? The fix isn't terribly urgent, but I'd like to confirm that this is a z3 issue and not some misunderstanding on my part. Thanks..

[aehyvari]

HI @LeventErkok , I agree, this is a bug.

[NikolajBjorner]

Added comments to the legacy versions exposed over the API to make it easier to develop a fix.

[LeventErkok]

@aehyvari

I think the bug is here:

$ git diff
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 3b52ca372..74cfc5e26 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -3088,7 +3088,7 @@ br_status bv_rewriter::mk_bvssub_overflow(unsigned num, expr * const * args, exp
     auto minSigned = mk_numeral(rational::power_of_two(sz-1), sz);
     expr_ref bvsaddo {m};
     expr * args2[2] = { args[0], m_util.mk_bv_neg(args[1]) };
-    auto bvsaddo_stat = mk_bvsadd_overflow(2, args2, bvsaddo);
+    auto bvsaddo_stat = mk_bvsadd_over_underflow(2, args2, bvsaddo);
     SASSERT(bvsaddo_stat != BR_FAILED); (void)bvsaddo_stat;
     auto first_arg_ge_zero = m_util.mk_sle(mk_zero(sz), args[0]);
     result = m.mk_ite(m.mk_eq(args[1], minSigned), first_arg_ge_zero, bvsaddo);

That is, the check should call mk_bvadd_over_underflow, not just mk_bvadd_overflow.

Making this change fixes the benchmark I quoted above. I'm not sure if there are other places that might have used the incorrect call as well. In fact, now that SMTLib doesn't really distinguish overflow from underflow, it might be best to merge these implementations and have just one version to simplify internal usage?

[NikolajBjorner]

the function name mk_bvsub_overflow seems misaligned with the semantics of bvssubo ?

[NikolajBjorner]

Yes, that aligns with what there is in the legacy API for the under-overflow semantics.