diff options
Diffstat (limited to 'test/regress/regress0/bv/fuzz13.smt')
| -rw-r--r-- | test/regress/regress0/bv/fuzz13.smt | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/fuzz13.smt b/test/regress/regress0/bv/fuzz13.smt new file mode 100644 index 000000000..6d84c00cb --- /dev/null +++ b/test/regress/regress0/bv/fuzz13.smt @@ -0,0 +1,23 @@ +(benchmark fuzzsmt +:logic QF_BV +:extrafuns ((v1 BitVec[13])) +:status sat +:formula +(let (?n1 bv1[13]) +(flet ($n2 (bvult v1 ?n1)) +(let (?n3 bv1[1]) +(let (?n4 bv0[1]) +(let (?n5 (ite $n2 ?n3 ?n4)) +(let (?n6 (zero_extend[12] ?n5)) +(flet ($n7 (bvuge ?n6 v1)) +(let (?n8 (ite $n7 ?n3 ?n4)) +(let (?n9 (zero_extend[12] ?n8)) +(flet ($n10 (bvult ?n9 ?n1)) +(let (?n11 (ite $n10 ?n3 ?n4)) +(let (?n12 (sign_extend[5] ?n5)) +(let (?n13 bv0[6]) +(flet ($n14 (bvsgt ?n12 ?n13)) +(let (?n15 (ite $n14 ?n3 ?n4)) +(flet ($n16 (= ?n11 ?n15)) +$n16 +))))))))))))))))) |