diff options
Diffstat (limited to 'test/regress/regress0/uflia/error0.delta01.smt')
-rw-r--r-- | test/regress/regress0/uflia/error0.delta01.smt | 78 |
1 files changed, 0 insertions, 78 deletions
diff --git a/test/regress/regress0/uflia/error0.delta01.smt b/test/regress/regress0/uflia/error0.delta01.smt deleted file mode 100644 index cc205063c..000000000 --- a/test/regress/regress0/uflia/error0.delta01.smt +++ /dev/null @@ -1,78 +0,0 @@ -(benchmark B_ -:logic QF_UFLIA -:extrafuns ((format Int Int)) -:extrafuns ((arg1 Int)) -:extrafuns ((fmt1 Int)) -:extrafuns ((s_count Int Int)) -:extrafuns ((fmt0 Int)) -:extrafuns ((x_count Int Int)) -:status sat -:formula -(flet ($n1 true) -(let (?n2 1) -(let (?n3 (~ ?n2)) -(let (?n4 (* ?n3 fmt1)) -(let (?n5 (+ ?n4 fmt0)) -(let (?n6 8) -(let (?n7 (~ ?n6)) -(flet ($n8 (>= ?n5 ?n7)) -(let (?n9 6) -(let (?n10 (x_count ?n9)) -(let (?n11 7) -(let (?n12 (x_count ?n11)) -(let (?n13 (* ?n3 ?n12)) -(let (?n14 (+ ?n10 ?n13)) -(let (?n15 0) -(flet ($n16 (>= ?n14 ?n15)) -(flet ($n17 (>= fmt1 ?n11)) -(flet ($n18 (<= arg1 ?n9)) -(let (?n19 2) -(let (?n20 (~ ?n19)) -(let (?n21 (* ?n3 fmt0)) -(let (?n22 (+ fmt1 ?n20 ?n21)) -(let (?n23 (s_count ?n22)) -(let (?n24 5) -(let (?n25 (s_count ?n24)) -(let (?n26 (* ?n3 ?n25)) -(let (?n27 (+ ?n23 ?n26)) -(flet ($n28 (= ?n15 ?n27)) -(flet ($n29 (not $n28)) -(let (?n30 (~ ?n11)) -(flet ($n31 (<= ?n5 ?n30)) -(flet ($n32 false) -(let (?n33 (+ arg1 ?n21)) -(flet ($n34 (<= ?n33 ?n2)) -(let (?n35 (+ ?n4 arg1)) -(flet ($n36 (<= ?n35 ?n15)) -(flet ($n37 (or $n32 $n32 $n34 $n36)) -(let (?n38 (x_count ?n2)) -(flet ($n39 (>= ?n38 ?n15)) -(let (?n40 (format ?n11)) -(flet ($n41 (<= ?n40 ?n15)) -(let (?n42 (x_count ?n22)) -(let (?n43 (+ ?n13 ?n42)) -(flet ($n44 (= ?n15 ?n43)) -(let (?n45 (s_count ?n9)) -(let (?n46 (* ?n3 ?n45)) -(let (?n47 (+ ?n23 ?n46)) -(flet ($n48 (= ?n15 ?n47)) -(flet ($n49 (or $n32 $n32 $n32 $n32 $n32 $n39 $n44 $n48)) -(let (?n50 (+ ?n2 fmt1)) -(let (?n51 (format ?n50)) -(flet ($n52 (>= ?n51 ?n15)) -(let (?n53 4) -(let (?n54 (format ?n53)) -(flet ($n55 (>= ?n54 ?n15)) -(let (?n56 9) -(let (?n57 (format ?n56)) -(flet ($n58 (<= ?n57 ?n15)) -(let (?n59 (format fmt1)) -(flet ($n60 (>= ?n59 ?n15)) -(let (?n61 12) -(let (?n62 (format ?n61)) -(flet ($n63 (>= ?n62 ?n15)) -(let (?n64 (format arg1)) -(flet ($n65 (= ?n15 ?n64)) -(flet ($n66 (and $n1 $n8 $n16 $n17 $n18 $n29 $n31 $n37 $n39 $n41 $n49 $n52 $n55 $n58 $n60 $n63 $n65)) -$n66 -))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) |