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, 0 insertions, 117 deletions
diff --git a/test/regress/regress0/bv/fuzz18.delta01.smt b/test/regress/regress0/bv/fuzz18.delta01.smt deleted file mode 100644 index 87cceb8e8..000000000 --- a/test/regress/regress0/bv/fuzz18.delta01.smt +++ /dev/null @@ -1,117 +0,0 @@ -(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 unsat -: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 -))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |