diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/smt/match_fail.sat.sail | 10 | ||||
| -rw-r--r-- | test/smt/rv_add_0.unsat.sail | 2 |
2 files changed, 11 insertions, 1 deletions
diff --git a/test/smt/match_fail.sat.sail b/test/smt/match_fail.sat.sail new file mode 100644 index 00000000..0a51b5f4 --- /dev/null +++ b/test/smt/match_fail.sat.sail @@ -0,0 +1,10 @@ +default Order dec + +$include <prelude.sail> + +$counterexample +function prop(xs: bits(4)) -> bool = { + match xs { + _ : bits(3) @ 0b0 => true + } +} diff --git a/test/smt/rv_add_0.unsat.sail b/test/smt/rv_add_0.unsat.sail index ed45112e..87c55487 100644 --- a/test/smt/rv_add_0.unsat.sail +++ b/test/smt/rv_add_0.unsat.sail @@ -145,7 +145,7 @@ function clause execute (ITYPE (imm, rs1, rd, RISCV_ADDI)) = function clause decode _ = None() -$property +$counterexample function prop(imm: bits(12), rs1: regbits, rd: regbits, v: xlenbits) -> bool = { X(rs1) = v; match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) { |