diff options
Diffstat (limited to 'test/regress/regress0/decision/error3.delta01.smt')
-rw-r--r-- | test/regress/regress0/decision/error3.delta01.smt | 32 |
1 files changed, 0 insertions, 32 deletions
diff --git a/test/regress/regress0/decision/error3.delta01.smt b/test/regress/regress0/decision/error3.delta01.smt deleted file mode 100644 index de4bccd77..000000000 --- a/test/regress/regress0/decision/error3.delta01.smt +++ /dev/null @@ -1,32 +0,0 @@ -(benchmark fuzzsmt -:logic QF_AUFBV -:extrafuns ((v1 BitVec[3])) -:extrafuns ((a2 Array[13:3])) -:status unsat -:formula -(let (?n1 bv0[3]) -(flet ($n2 (bvsgt v1 v1)) -(let (?n3 bv1[1]) -(let (?n4 bv0[1]) -(let (?n5 (ite $n2 ?n3 ?n4)) -(let (?n6 (sign_extend[2] ?n5)) -(flet ($n7 (bvslt ?n6 v1)) -(let (?n8 (ite $n7 ?n3 ?n4)) -(let (?n9 (sign_extend[2] ?n8)) -(let (?n10 bv0[13]) -(let (?n11 (select a2 ?n10)) -(let (?n12 (bvshl ?n9 ?n11)) -(flet ($n13 (= ?n1 ?n12)) -(flet ($n14 (not $n13)) -(let (?n15 (bvnot ?n8)) -(let (?n16 (zero_extend[10] ?n15)) -(let (?n17 bv0[11]) -(flet ($n18 (= ?n16 ?n17)) -(flet ($n19 (not $n18)) -(let (?n20 (repeat[2] ?n15)) -(let (?n21 (zero_extend[9] ?n20)) -(flet ($n22 (bvult ?n17 ?n21)) -(flet ($n23 (and $n19 $n22)) -(flet ($n24 (and $n14 $n23)) -$n24 -))))))))))))))))))))))))) |