We ran into the following SMTLIBv2 query:
(declare-fun x () (_ BitVec 16))
(assert (and (bvsle x (_ bv65472 16) ) (bvsgt x (_ bv65416 16) ) ) )
This query is
, i.e., there is an
in the interval
. I double-checked it with stp/cvc4/boolector.
(unstable branch, commit