test/smt/exception_3.unsat.sail


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

default Order dec

$include <vector_dec.sail>

union exception = {
  E_bool : bool,
  E_unit : unit
}

register R : bool

function check_sat((): unit) -> bool = {
  try {
    if R then {
       throw(E_bool(false))
    } else {
       return(false);
       true
    }
  } catch {
    E_bool(b) => b,
    E_unit() => true
  }
}