summaryrefslogtreecommitdiff
path: root/test/smt/rv_add_0.unsat.sail
diff options
context:
space:
mode:
Diffstat (limited to 'test/smt/rv_add_0.unsat.sail')
-rw-r--r--test/smt/rv_add_0.unsat.sail2
1 files changed, 1 insertions, 1 deletions
diff --git a/test/smt/rv_add_0.unsat.sail b/test/smt/rv_add_0.unsat.sail
index 87c55487..ed45112e 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()
-$counterexample
+$property
function prop(imm: bits(12), rs1: regbits, rd: regbits, v: xlenbits) -> bool = {
X(rs1) = v;
match decode(imm @ rs1 @ 0b000 @ rd @ 0b0010011) {