From: Dejan Jovanović Date: Mon, 11 Jun 2012 21:53:00 +0000 (+0000) Subject: another benchmark that used to fail X-Git-Tag: cvc5-1.0.0~8081 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dbe06dccdb08c816fd28266f44585e2d7f6a0a9f;p=cvc5.git another benchmark that used to fail --- diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index 995ade606..954050a97 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -33,6 +33,7 @@ SMT_TESTS = \ fuzz16.delta01.smt \ fuzz17.delta01.smt \ fuzz18.delta01.smt \ + fuzz18.delta02.smt \ fuzz18.smt \ fuzz19.delta01.smt \ fuzz19.smt \ diff --git a/test/regress/regress0/bv/fuzz18.delta02.smt b/test/regress/regress0/bv/fuzz18.delta02.smt new file mode 100644 index 000000000..e0fb866d7 --- /dev/null +++ b/test/regress/regress0/bv/fuzz18.delta02.smt @@ -0,0 +1,115 @@ +(benchmark fuzzsmt +:logic QF_BV +:extrafuns ((v5 BitVec[4])) +:extrafuns ((v0 BitVec[4])) +:extrafuns ((v8 BitVec[4])) +:extrafuns ((v3 BitVec[4])) +:extrafuns ((v2 BitVec[4])) +:extrafuns ((v6 BitVec[4])) +:extrafuns ((v1 BitVec[4])) +:status sat +:formula +(flet ($n1 true) +(let (?n2 bv1[1]) +(let (?n3 (extract[1:1] v2)) +(flet ($n4 (= ?n2 ?n3)) +(let (?n5 bv4[4]) +(let (?n6 (bvadd v1 v6)) +(let (?n7 (bvsub ?n6 v6)) +(let (?n8 (ite $n4 ?n5 ?n7)) +(flet ($n9 (bvule ?n8 v2)) +(let (?n10 bv0[1]) +(let (?n11 (ite $n9 ?n2 ?n10)) +(let (?n12 (zero_extend[3] ?n11)) +(let (?n13 bv1[4]) +(flet ($n14 (bvsge ?n12 ?n13)) +(flet ($n15 false) +(let (?n16 bv0[4]) +(let (?n17 (bvand ?n5 v3)) +(let (?n18 (bvlshr v1 ?n17)) +(flet ($n19 (bvslt ?n5 v2)) +(let (?n20 (ite $n19 ?n2 ?n10)) +(let (?n21 (zero_extend[3] ?n20)) +(flet ($n22 (bvugt ?n18 ?n21)) +(let (?n23 (ite $n22 ?n2 ?n10)) +(let (?n24 (zero_extend[3] ?n23)) +(flet ($n25 (bvsge ?n16 ?n24)) +(let (?n26 (ite $n25 ?n2 ?n10)) +(let (?n27 (sign_extend[3] ?n26)) +(flet ($n28 (bvugt ?n13 ?n27)) +(flet ($n29 (bvsle ?n16 v1)) +(let (?n30 (ite $n29 ?n2 ?n10)) +(let (?n31 (zero_extend[3] ?n30)) +(flet ($n32 (bvslt ?n16 ?n31)) +(let (?n33 (ite $n32 ?n2 ?n10)) +(let (?n34 (zero_extend[3] ?n33)) +(flet ($n35 (bvslt ?n34 ?n13)) +(flet ($n36 (or $n15 $n28 $n35)) +(flet ($n37 (bvuge v0 v6)) +(let (?n38 (ite $n37 ?n2 ?n10)) +(let (?n39 (sign_extend[3] ?n38)) +(flet ($n40 (bvule ?n39 ?n16)) +(let (?n41 (ite $n40 ?n2 ?n10)) +(let (?n42 (zero_extend[3] ?n41)) +(flet ($n43 (bvule ?n42 ?n16)) +(flet ($n44 (bvuge v1 v6)) +(let (?n45 (ite $n44 ?n2 ?n10)) +(flet ($n46 (= ?n2 ?n45)) +(let (?n47 (ite $n46 ?n13 ?n16)) +(flet ($n48 (bvsge ?n47 ?n16)) +(flet ($n49 (not $n48)) +(flet ($n50 (or $n15 $n43 $n49)) +(let (?n51 (bvshl ?n5 v1)) +(flet ($n52 (bvule ?n51 ?n16)) +(let (?n53 (sign_extend[3] ?n45)) +(flet ($n54 (bvult v0 ?n53)) +(let (?n55 (ite $n54 ?n2 ?n10)) +(let (?n56 (bvlshr ?n2 ?n55)) +(flet ($n57 (= ?n2 ?n56)) +(flet ($n58 (bvuge ?n16 ?n51)) +(let (?n59 (ite $n58 ?n2 ?n10)) +(let (?n60 (zero_extend[3] ?n59)) +(flet ($n61 (bvugt ?n60 ?n16)) +(flet ($n62 (bvslt v6 ?n16)) +(let (?n63 (ite $n62 ?n2 ?n10)) +(flet ($n64 (distinct ?n2 ?n63)) +(flet ($n65 (or $n15 $n61 $n64)) +(flet ($n66 (bvsgt v3 ?n31)) +(let (?n67 (ite $n66 ?n2 ?n10)) +(let (?n68 (zero_extend[3] ?n67)) +(flet ($n69 (= v1 ?n68)) +(let (?n70 (bvnot v5)) +(flet ($n71 (bvule v6 ?n70)) +(flet ($n72 (or $n15 $n69 $n71)) +(flet ($n73 (bvule v0 v6)) +(let (?n74 (ite $n73 ?n2 ?n10)) +(let (?n75 (extract[2:2] ?n47)) +(flet ($n76 (bvule ?n74 ?n75)) +(flet ($n77 (bvsle ?n16 ?n17)) +(flet ($n78 (or $n15 $n76 $n77)) +(let (?n79 (bvadd ?n13 ?n13)) +(let (?n80 (bvshl ?n18 ?n79)) +(flet ($n81 (bvsge ?n16 ?n80)) +(flet ($n82 (not $n81)) +(let (?n83 (bvand ?n5 ?n70)) +(flet ($n84 (bvuge ?n16 ?n83)) +(flet ($n85 (not $n84)) +(flet ($n86 (or $n15 $n82 $n85)) +(let (?n87 (sign_extend[3] ?n2)) +(flet ($n88 (bvuge v6 ?n87)) +(let (?n89 (ite $n88 ?n2 ?n10)) +(flet ($n90 (bvslt ?n23 ?n89)) +(let (?n91 (bvand v1 v6)) +(let (?n92 (bvxnor ?n16 ?n91)) +(let (?n93 (bvxnor ?n16 ?n92)) +(flet ($n94 (bvsle ?n79 ?n93)) +(flet ($n95 (not $n94)) +(let (?n96 (bvcomp v2 v3)) +(flet ($n97 (= ?n2 ?n96)) +(let (?n98 (bvcomp v0 v5)) +(let (?n99 (zero_extend[3] ?n98)) +(let (?n100 (ite $n97 v8 ?n99)) +(flet ($n101 (distinct ?n16 ?n100)) +(flet ($n102 (and $n14 $n36 $n50 $n52 $n57 $n65 $n72 $n78 $n86 $n90 $n95 $n101)) +$n102 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))