diff options
Diffstat (limited to 'test/regress/regress0/uflia')
6 files changed, 283 insertions, 0 deletions
diff --git a/test/regress/regress0/uflia/Makefile.am b/test/regress/regress0/uflia/Makefile.am index 0244d768e..5b095b500 100644 --- a/test/regress/regress0/uflia/Makefile.am +++ b/test/regress/regress0/uflia/Makefile.am @@ -14,7 +14,12 @@ MAKEFLAGS = -k # Regression tests for SMT inputs SMT_TESTS = \ xs-09-16-3-4-1-5.smt \ + xs-09-16-3-4-1-5.delta01.smt \ + xs-09-16-3-4-1-5.delta02.smt \ + xs-09-16-3-4-1-5.delta03.smt \ + xs-09-16-3-4-1-5.delta04.smt \ error0.smt2 \ + error0.delta01.smt \ simple_cyclic2.smt2 # Regression tests for SMT2 inputs diff --git a/test/regress/regress0/uflia/error0.delta01.smt b/test/regress/regress0/uflia/error0.delta01.smt new file mode 100644 index 000000000..cc205063c --- /dev/null +++ b/test/regress/regress0/uflia/error0.delta01.smt @@ -0,0 +1,78 @@ +(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 +))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt new file mode 100644 index 000000000..c7fed0c15 --- /dev/null +++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt @@ -0,0 +1,48 @@ +(benchmark mathsat +:logic QF_UFLIA +:extrafuns ((s_count Int Int)) +:extrafuns ((fmt1 Int)) +:extrafuns ((fmt_length Int)) +:status unsat +:formula +(let (?n1 0) +(let (?n2 6) +(let (?n3 (s_count ?n2)) +(flet ($n4 (= ?n1 ?n3)) +(let (?n5 5) +(let (?n6 (s_count ?n5)) +(flet ($n7 (= ?n1 ?n6)) +(let (?n8 4) +(let (?n9 (s_count ?n8)) +(flet ($n10 (= ?n1 ?n9)) +(let (?n11 3) +(let (?n12 (s_count ?n11)) +(flet ($n13 (= ?n1 ?n12)) +(let (?n14 1) +(let (?n15 (s_count ?n1)) +(flet ($n16 (= ?n14 ?n15)) +(let (?n17 (s_count ?n14)) +(flet ($n18 (= ?n1 ?n17)) +(flet ($n19 (and $n16 $n18)) +(let (?n20 2) +(let (?n21 (s_count ?n20)) +(flet ($n22 (= ?n1 ?n21)) +(flet ($n23 (and $n19 $n22)) +(flet ($n24 (and $n13 $n23)) +(flet ($n25 (and $n10 $n24)) +(flet ($n26 (and $n7 $n25)) +(flet ($n27 (and $n4 $n26)) +(let (?n28 9) +(flet ($n29 (= ?n28 fmt_length)) +(flet ($n30 (> fmt1 ?n14)) +(flet ($n31 (< fmt1 fmt_length)) +(flet ($n32 (and $n30 $n31)) +(let (?n33 (- fmt1 ?n20)) +(let (?n34 (s_count ?n33)) +(let (?n35 (+ ?n14 ?n34)) +(flet ($n36 (= ?n1 ?n35)) +(flet ($n37 (and $n32 $n36)) +(flet ($n38 (and $n29 $n37)) +(flet ($n39 (and $n27 $n38)) +$n39 +)))))))))))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smt new file mode 100644 index 000000000..fb16651ff --- /dev/null +++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smt @@ -0,0 +1,40 @@ +(benchmark mathsat +:logic QF_UFLIA +:extrafuns ((arg1 Int)) +:extrafuns ((adr_lo Int)) +:extrafuns ((select_format Int Int)) +:extrafuns ((x Int)) +:status sat +:formula +(let (?n1 (select_format arg1)) +(flet ($n2 (= ?n1 adr_lo)) +(let (?n3 0) +(flet ($n4 (= ?n3 x)) +(let (?n5 4) +(let (?n6 (select_format ?n5)) +(flet ($n7 (= adr_lo ?n6)) +(let (?n8 3) +(let (?n9 (select_format ?n8)) +(flet ($n10 (= adr_lo ?n9)) +(let (?n11 2) +(let (?n12 (select_format ?n11)) +(flet ($n13 (= adr_lo ?n12)) +(let (?n14 1) +(let (?n15 (select_format ?n3)) +(flet ($n16 (= ?n14 ?n15)) +(let (?n17 (select_format ?n14)) +(flet ($n18 (= ?n3 ?n17)) +(flet ($n19 (or $n16 $n18)) +(flet ($n20 (or $n13 $n19)) +(flet ($n21 (or $n10 $n20)) +(flet ($n22 (or $n7 $n21)) +(flet ($n23 (or $n4 $n22)) +(flet ($n24 (= adr_lo ?n8)) +(flet ($n25 (< arg1 ?n5)) +(flet ($n26 (>= arg1 ?n3)) +(flet ($n27 (and $n25 $n26)) +(flet ($n28 (and $n24 $n27)) +(flet ($n29 (and $n23 $n28)) +(flet ($n30 (and $n2 $n29)) +$n30 +))))))))))))))))))))))))))))))) diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smt new file mode 100644 index 000000000..6f65e83ec --- /dev/null +++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smt @@ -0,0 +1,45 @@ +(benchmark mathsat +:logic QF_UFLIA +:extrafuns ((fmt_length Int)) +:extrafuns ((fmt1 Int)) +:extrafuns ((arg1 Int)) +:extrafuns ((select_format Int Int)) +:status sat +:formula +(let (?n1 1) +(let (?n2 (+ ?n1 fmt1)) +(let (?n3 (select_format ?n2)) +(flet ($n4 (= ?n1 ?n3)) +(let (?n5 (select_format arg1)) +(let (?n6 0) +(flet ($n7 (= ?n5 ?n6)) +(flet ($n8 (and $n4 $n7)) +(let (?n9 7) +(let (?n10 (select_format ?n9)) +(flet ($n11 (= ?n1 ?n10)) +(let (?n12 (select_format ?n6)) +(flet ($n13 (= ?n1 ?n12)) +(let (?n14 (select_format ?n1)) +(flet ($n15 (= ?n1 ?n14)) +(flet ($n16 (or $n13 $n15)) +(let (?n17 5) +(let (?n18 (select_format ?n17)) +(flet ($n19 (= ?n6 ?n18)) +(flet ($n20 (or $n16 $n19)) +(let (?n21 6) +(let (?n22 (select_format ?n21)) +(flet ($n23 (= ?n6 ?n22)) +(flet ($n24 (or $n20 $n23)) +(flet ($n25 (or $n11 $n24)) +(let (?n26 9) +(flet ($n27 (= ?n26 fmt_length)) +(let (?n28 2) +(let (?n29 (- fmt1 ?n28)) +(flet ($n30 (= arg1 ?n29)) +(flet ($n31 (< fmt1 fmt_length)) +(flet ($n32 (and $n30 $n31)) +(flet ($n33 (and $n27 $n32)) +(flet ($n34 (and $n25 $n33)) +(flet ($n35 (and $n8 $n34)) +$n35 +)))))))))))))))))))))))))))))))))))) 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 new file mode 100644 index 000000000..f1212a876 --- /dev/null +++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt @@ -0,0 +1,67 @@ +(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 +)))))))))))))))))))))))))))))))))))))))))))))))))))))))) |