diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-14 01:08:11 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-14 01:08:11 +0000 |
commit | dd713fdbc16b07adc8011dea09b53fb3bc168662 (patch) | |
tree | cc58788ed58fd86c5aaa58c0fafa2bbb0f8b6567 /test/regress/regress0/aufbv | |
parent | 1267706e0c508ada17d75c07c4606eb108ae5309 (diff) |
* removing rewriteEquality from the rewriter
* theories now get either an assertion from the SAT solver (normalized) or an (dis-)equality between two shared terms that is non-normalized
Diffstat (limited to 'test/regress/regress0/aufbv')
-rw-r--r-- | test/regress/regress0/aufbv/Makefile.am | 1 | ||||
-rw-r--r-- | test/regress/regress0/aufbv/bug348.smt | 133 |
2 files changed, 134 insertions, 0 deletions
diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index 263795814..efffc7afd 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -14,6 +14,7 @@ TESTS = \ bug00.smt \ bug338.smt2 \ bug347.smt \ + bug348.smt \ try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt \ diseqprop.01.smt \ wchains010ue.delta01.smt \ diff --git a/test/regress/regress0/aufbv/bug348.smt b/test/regress/regress0/aufbv/bug348.smt new file mode 100644 index 000000000..46172eba9 --- /dev/null +++ b/test/regress/regress0/aufbv/bug348.smt @@ -0,0 +1,133 @@ +(benchmark B_ +:logic QF_AUFBV +:extrafuns ((start2 BitVec[32])) +:extrafuns ((start1 BitVec[32])) +:extrafuns ((a1 Array[32:8])) +:status unsat +:formula +(let (?n1 bv0[1]) +(let (?n2 bv0[8]) +(let (?n3 (store a1 start1 ?n2)) +(let (?n4 bv3[32]) +(let (?n5 (bvadd ?n4 start1)) +(let (?n6 (store ?n3 ?n5 ?n2)) +(let (?n7 bv0[32]) +(let (?n8 (select ?n6 ?n7)) +(let (?n9 (bvnot ?n8)) +(let (?n10 (select ?n6 ?n7)) +(let (?n11 (bvnot ?n10)) +(let (?n12 (bvand ?n9 ?n11)) +(let (?n13 (bvnot ?n12)) +(let (?n14 (bvand ?n8 ?n10)) +(let (?n15 (bvnot ?n14)) +(let (?n16 (bvand ?n13 ?n15)) +(let (?n17 (bvnot ?n16)) +(let (?n18 (bvand ?n9 ?n17)) +(let (?n19 (bvnot ?n18)) +(let (?n20 (bvand ?n8 ?n16)) +(let (?n21 (bvnot ?n20)) +(let (?n22 (bvand ?n19 ?n21)) +(let (?n23 (store ?n6 ?n7 ?n22)) +(let (?n24 (bvnot ?n22)) +(let (?n25 (bvand ?n17 ?n24)) +(let (?n26 (bvnot ?n25)) +(let (?n27 (bvand ?n16 ?n22)) +(let (?n28 (bvnot ?n27)) +(let (?n29 (bvand ?n26 ?n28)) +(let (?n30 (store ?n23 ?n7 ?n29)) +(let (?n31 (bvadd ?n4 start2)) +(let (?n32 (select ?n30 ?n31)) +(let (?n33 (bvnot ?n32)) +(let (?n34 (select ?n30 start2)) +(let (?n35 (bvnot ?n34)) +(let (?n36 (bvand ?n33 ?n35)) +(let (?n37 (bvnot ?n36)) +(let (?n38 (bvand ?n32 ?n34)) +(let (?n39 (bvnot ?n38)) +(let (?n40 (bvand ?n37 ?n39)) +(let (?n41 (bvnot ?n40)) +(let (?n42 (bvand ?n33 ?n41)) +(let (?n43 (bvnot ?n42)) +(let (?n44 (bvand ?n32 ?n40)) +(let (?n45 (bvnot ?n44)) +(let (?n46 (bvand ?n43 ?n45)) +(let (?n47 (store ?n30 ?n31 ?n46)) +(let (?n48 (bvnot ?n46)) +(let (?n49 (bvand ?n41 ?n48)) +(let (?n50 (bvnot ?n49)) +(let (?n51 (bvand ?n40 ?n46)) +(let (?n52 (bvnot ?n51)) +(let (?n53 (bvand ?n50 ?n52)) +(let (?n54 (store ?n47 start2 ?n53)) +(let (?n55 (select ?n54 ?n7)) +(let (?n56 (bvnot ?n55)) +(let (?n57 (select ?n54 start2)) +(let (?n58 (bvnot ?n57)) +(let (?n59 (bvand ?n56 ?n58)) +(let (?n60 (bvnot ?n59)) +(let (?n61 (bvand ?n55 ?n57)) +(let (?n62 (bvnot ?n61)) +(let (?n63 (bvand ?n60 ?n62)) +(let (?n64 (bvnot ?n63)) +(let (?n65 (bvand ?n56 ?n64)) +(let (?n66 (bvnot ?n65)) +(let (?n67 (bvand ?n55 ?n63)) +(let (?n68 (bvnot ?n67)) +(let (?n69 (bvand ?n66 ?n68)) +(let (?n70 (store ?n54 ?n7 ?n69)) +(let (?n71 (bvnot ?n69)) +(let (?n72 (bvand ?n64 ?n71)) +(let (?n73 (bvnot ?n72)) +(let (?n74 (bvand ?n63 ?n69)) +(let (?n75 (bvnot ?n74)) +(let (?n76 (bvand ?n73 ?n75)) +(let (?n77 (store ?n70 start2 ?n76)) +(let (?n78 (select ?n77 ?n7)) +(let (?n79 (bvnot ?n78)) +(let (?n80 (select ?n77 ?n7)) +(let (?n81 (bvnot ?n80)) +(let (?n82 (bvand ?n79 ?n81)) +(let (?n83 (bvnot ?n82)) +(let (?n84 (bvand ?n78 ?n80)) +(let (?n85 (bvnot ?n84)) +(let (?n86 (bvand ?n83 ?n85)) +(let (?n87 (bvnot ?n86)) +(let (?n88 (bvand ?n79 ?n87)) +(let (?n89 (bvnot ?n88)) +(let (?n90 (bvand ?n78 ?n86)) +(let (?n91 (bvnot ?n90)) +(let (?n92 (bvand ?n89 ?n91)) +(let (?n93 (store ?n77 ?n7 ?n92)) +(let (?n94 (bvnot ?n92)) +(let (?n95 (bvand ?n87 ?n94)) +(let (?n96 (bvnot ?n95)) +(let (?n97 (bvand ?n86 ?n92)) +(let (?n98 (bvnot ?n97)) +(let (?n99 (bvand ?n96 ?n98)) +(let (?n100 (store ?n93 ?n7 ?n99)) +(let (?n101 (store a1 ?n5 ?n2)) +(let (?n102 (store ?n101 start1 ?n2)) +(let (?n103 (select ?n102 ?n7)) +(let (?n104 (store ?n102 ?n7 ?n103)) +(let (?n105 (select ?n102 ?n7)) +(let (?n106 (store ?n104 ?n7 ?n105)) +(let (?n107 (select ?n106 start2)) +(let (?n108 (store ?n106 ?n31 ?n107)) +(let (?n109 (select ?n106 ?n31)) +(let (?n110 (store ?n108 start2 ?n109)) +(let (?n111 (select ?n110 start2)) +(let (?n112 (store ?n110 ?n7 ?n111)) +(let (?n113 (select ?n110 ?n7)) +(let (?n114 (store ?n112 start2 ?n113)) +(let (?n115 (select ?n114 ?n7)) +(let (?n116 (store ?n114 ?n7 ?n115)) +(let (?n117 (select ?n114 ?n7)) +(let (?n118 (store ?n116 ?n7 ?n117)) +(flet ($n119 (= ?n100 ?n118)) +(let (?n120 bv1[1]) +(let (?n121 (ite $n119 ?n120 ?n1)) +(let (?n122 (bvnot ?n121)) +(flet ($n123 (= ?n1 ?n122)) +(flet ($n124 (not $n123)) +$n124 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |