diff options
Diffstat (limited to 'test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt')
-rw-r--r-- | test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt | 67 |
1 files changed, 0 insertions, 67 deletions
diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt deleted file mode 100644 index f1212a876..000000000 --- a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt +++ /dev/null @@ -1,67 +0,0 @@ -(benchmark mathsat -:logic QF_UFLIA -:extrafuns ((fmt_length Int)) -:extrafuns ((fmt1 Int)) -:extrafuns ((x_count Int Int)) -:extrafuns ((select_format Int Int)) -:extrafuns ((percent Int)) -:extrafuns ((s_count Int Int)) -:status sat -:formula -(let (?n1 1) -(let (?n2 5) -(let (?n3 (x_count ?n2)) -(flet ($n4 (= ?n1 ?n3)) -(let (?n5 4) -(let (?n6 (x_count ?n5)) -(flet ($n7 (= ?n1 ?n6)) -(let (?n8 3) -(let (?n9 (x_count ?n8)) -(let (?n10 2) -(let (?n11 (x_count ?n10)) -(flet ($n12 (= ?n9 ?n11)) -(let (?n13 0) -(let (?n14 (select_format ?n8)) -(flet ($n15 (= ?n13 ?n14)) -(let (?n16 (x_count ?n13)) -(flet ($n17 (= ?n1 ?n16)) -(flet ($n18 (= ?n1 percent)) -(flet ($n19 true) -(let (?n20 (s_count ?n13)) -(flet ($n21 (= ?n13 ?n20)) -(flet ($n22 (if_then_else $n18 $n19 $n21)) -(let (?n23 (select_format ?n10)) -(flet ($n24 (= percent ?n23)) -(flet ($n25 (= ?n1 ?n14)) -(flet ($n26 (and $n24 $n25)) -(flet ($n27 false) -(flet ($n28 (if_then_else $n26 $n27 $n19)) -(flet ($n29 (and $n22 $n28)) -(flet ($n30 (and $n17 $n29)) -(flet ($n31 (= ?n13 percent)) -(flet ($n32 (= ?n13 ?n23)) -(flet ($n33 (and $n31 $n32)) -(let (?n34 (x_count ?n1)) -(flet ($n35 (= ?n13 ?n34)) -(flet ($n36 (= ?n16 ?n34)) -(flet ($n37 (if_then_else $n33 $n35 $n36)) -(flet ($n38 (and $n30 $n37)) -(flet ($n39 (and $n15 $n38)) -(flet ($n40 (and $n12 $n39)) -(flet ($n41 (and $n7 $n40)) -(flet ($n42 (and $n4 $n41)) -(let (?n43 9) -(flet ($n44 (= ?n43 fmt_length)) -(let (?n45 (- fmt1 ?n10)) -(let (?n46 (x_count ?n45)) -(let (?n47 (+ ?n1 ?n46)) -(flet ($n48 (= ?n13 ?n47)) -(flet ($n49 (> fmt1 ?n1)) -(let (?n50 (- fmt_length ?n1)) -(flet ($n51 (< fmt1 ?n50)) -(flet ($n52 (and $n49 $n51)) -(flet ($n53 (and $n48 $n52)) -(flet ($n54 (and $n44 $n53)) -(flet ($n55 (and $n42 $n54)) -$n55 -)))))))))))))))))))))))))))))))))))))))))))))))))))))))) |