diff options
Diffstat (limited to 'test/regress/regress0/bv/fuzz18.delta01.smt')
-rw-r--r-- | test/regress/regress0/bv/fuzz18.delta01.smt | 117 |
1 files changed, 117 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/fuzz18.delta01.smt b/test/regress/regress0/bv/fuzz18.delta01.smt new file mode 100644 index 000000000..6622ebc15 --- /dev/null +++ b/test/regress/regress0/bv/fuzz18.delta01.smt @@ -0,0 +1,117 @@ +(benchmark fuzzsmt +:logic QF_BV +:extrafuns ((v2 BitVec[4])) +:extrafuns ((v4 BitVec[4])) +:extrafuns ((v1 BitVec[4])) +:extrafuns ((v0 BitVec[4])) +:extrafuns ((v6 BitVec[4])) +:status unknown +:formula +(let (?n1 bv1[1]) +(let (?n2 (extract[1:1] v2)) +(flet ($n3 (= ?n1 ?n2)) +(let (?n4 bv0[4]) +(let (?n5 bv1[4]) +(let (?n6 (ite $n3 ?n4 ?n5)) +(let (?n7 (bvlshr v2 v4)) +(flet ($n8 (bvule ?n6 ?n7)) +(let (?n9 bv0[1]) +(let (?n10 (ite $n8 ?n1 ?n9)) +(flet ($n11 (distinct ?n1 ?n10)) +(let (?n12 (ite $n11 ?n1 ?n9)) +(let (?n13 (sign_extend[3] ?n12)) +(flet ($n14 (bvuge ?n13 ?n5)) +(flet ($n15 (bvuge v1 v6)) +(let (?n16 (ite $n15 ?n1 ?n9)) +(let (?n17 (sign_extend[3] ?n16)) +(let (?n18 (bvand v1 ?n17)) +(flet ($n19 (bvult ?n18 ?n5)) +(let (?n20 (ite $n19 ?n1 ?n9)) +(flet ($n21 (bvslt ?n1 ?n20)) +(let (?n22 (ite $n21 ?n1 ?n9)) +(let (?n23 (zero_extend[1] ?n22)) +(let (?n24 bv0[2]) +(flet ($n25 (bvsgt ?n23 ?n24)) +(let (?n26 (ite $n25 ?n1 ?n9)) +(let (?n27 (sign_extend[3] ?n26)) +(flet ($n28 (bvsle v2 ?n27)) +(let (?n29 (rotate_left[3] v4)) +(let (?n30 (bvnot ?n29)) +(flet ($n31 (bvslt ?n4 ?n30)) +(let (?n32 (ite $n31 ?n1 ?n9)) +(let (?n33 (zero_extend[3] ?n32)) +(flet ($n34 (bvsge ?n5 ?n33)) +(let (?n35 (bvsub ?n5 ?n30)) +(let (?n36 bv4[4]) +(flet ($n37 (bvule ?n35 ?n36)) +(flet ($n38 false) +(flet ($n39 (bvult v0 ?n5)) +(let (?n40 (bvshl ?n36 v1)) +(let (?n41 (bvmul v4 ?n18)) +(flet ($n42 (distinct ?n40 ?n41)) +(let (?n43 (ite $n42 ?n1 ?n9)) +(let (?n44 bv1[2]) +(let (?n45 (bvnor v1 ?n30)) +(flet ($n46 (bvuge ?n45 v6)) +(let (?n47 (ite $n46 ?n1 ?n9)) +(let (?n48 (sign_extend[3] ?n47)) +(flet ($n49 (bvult ?n4 ?n48)) +(let (?n50 (ite $n49 ?n1 ?n9)) +(let (?n51 (sign_extend[1] ?n50)) +(flet ($n52 (bvule ?n44 ?n51)) +(let (?n53 (ite $n52 ?n1 ?n9)) +(flet ($n54 (= ?n43 ?n53)) +(let (?n55 (ite $n54 ?n1 ?n9)) +(let (?n56 (sign_extend[3] ?n55)) +(flet ($n57 (bvugt ?n5 ?n56)) +(flet ($n58 (or $n38 $n39 $n57)) +(let (?n59 (sign_extend[3] ?n1)) +(let (?n60 (bvmul v2 ?n36)) +(let (?n61 (bvnor ?n5 ?n60)) +(let (?n62 (bvadd ?n59 ?n61)) +(flet ($n63 (bvsge ?n62 ?n4)) +(flet ($n64 (bvugt ?n59 v2)) +(flet ($n65 (bvsge v6 ?n61)) +(let (?n66 (ite $n65 ?n1 ?n9)) +(let (?n67 (bvshl v1 v0)) +(flet ($n68 (bvuge ?n4 ?n40)) +(let (?n69 (ite $n68 ?n1 ?n9)) +(let (?n70 (bvxnor ?n9 ?n69)) +(let (?n71 (sign_extend[3] ?n70)) +(flet ($n72 (bvuge v6 ?n71)) +(let (?n73 (ite $n72 ?n1 ?n9)) +(let (?n74 (zero_extend[3] ?n73)) +(flet ($n75 (bvsle ?n67 ?n74)) +(let (?n76 (ite $n75 ?n1 ?n9)) +(flet ($n77 (bvugt ?n66 ?n76)) +(flet ($n78 (or $n38 $n64 $n77)) +(flet ($n79 (bvult ?n4 ?n18)) +(let (?n80 (ite $n79 ?n1 ?n9)) +(flet ($n81 (bvule ?n1 ?n80)) +(flet ($n82 (not $n81)) +(let (?n83 (sign_extend[1] ?n66)) +(flet ($n84 (= ?n24 ?n83)) +(flet ($n85 (or $n38 $n82 $n84)) +(flet ($n86 (bvuge ?n29 ?n62)) +(flet ($n87 (bvsgt ?n45 ?n4)) +(let (?n88 (ite $n87 ?n1 ?n9)) +(flet ($n89 (bvsge ?n10 ?n88)) +(flet ($n90 (bvsgt ?n4 v0)) +(let (?n91 (ite $n90 ?n1 ?n9)) +(let (?n92 (zero_extend[3] ?n91)) +(flet ($n93 (bvsgt v0 ?n92)) +(flet ($n94 (or $n38 $n89 $n93)) +(let (?n95 (bvcomp ?n4 ?n7)) +(let (?n96 (sign_extend[3] ?n95)) +(flet ($n97 (bvugt ?n96 ?n5)) +(let (?n98 (ite $n97 ?n1 ?n9)) +(flet ($n99 (bvsgt ?n98 ?n1)) +(flet ($n100 (bvule ?n45 ?n5)) +(let (?n101 (ite $n100 ?n1 ?n9)) +(flet ($n102 (bvslt ?n101 ?n9)) +(flet ($n103 (bvsge v2 ?n59)) +(let (?n104 (ite $n103 ?n1 ?n9)) +(flet ($n105 (bvugt ?n104 ?n9)) +(flet ($n106 (and $n14 $n28 $n34 $n37 $n58 $n63 $n78 $n85 $n86 $n94 $n99 $n102 $n105)) +$n106 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |