summaryrefslogtreecommitdiff
path: root/test/smt/let_intervene.unsat.sail
blob: 5494848b3e7aec92e15167a4442fb74f98d52c07 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
default Order dec

$include <prelude.sail>

$property
val prop : unit -> bool

let C = 0
let x = bitone

function prop() = {
  let n = 3;
  bv = 0x0;
  foreach (i from C to n) {
    bv[i] = x
  };
  bv == 0xF
}