test/smt/sign_extend_2.unsat.sail


1
2
3
4
5
6
7
8
9
10
11
12
13
14

default Order dec

$include <prelude.sail>

$property
function prop(xs: bits(16)) -> bool = {
  var p: bool = true;
  if xs[15] == bitzero then {
    p = 0x0000 @ xs == sail_sign_extend(xs, 32);
  } else {
    p = 0xFFFF @ xs == sail_sign_extend(xs, 32);
  };
  p
}