From 9bcda83d2d322a97b5896ce160c298f6a159a2d2 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 15 Dec 2011 20:39:20 +0000 Subject: [PATCH] Partial fix in arithmetic for propagating shared terms. This partially resolves bug 289. Adds failing tests to regress1. --- src/theory/arith/theory_arith.cpp | 38 +++++++++++++++++++-- test/regress/regress1/Makefile.am | 8 +++-- test/regress/regress1/hash_sat_06_19.smt2 | 33 ++++++++++++++++++ test/regress/regress1/hash_sat_07_17.smt2 | 32 +++++++++++++++++ test/regress/regress1/hash_sat_09_09.smt2 | 26 ++++++++++++++ test/regress/regress1/hash_sat_10_09.smt2 | 27 +++++++++++++++ test/regress/regress1/ooo.tag10.smt2 | 28 +++++++++++++++ test/regress/regress1/xs-11-20-5-2-5-3.smt2 | 24 +++++++++++++ 8 files changed, 212 insertions(+), 4 deletions(-) create mode 100644 test/regress/regress1/hash_sat_06_19.smt2 create mode 100644 test/regress/regress1/hash_sat_07_17.smt2 create mode 100644 test/regress/regress1/hash_sat_09_09.smt2 create mode 100644 test/regress/regress1/hash_sat_10_09.smt2 create mode 100644 test/regress/regress1/ooo.tag10.smt2 create mode 100644 test/regress/regress1/xs-11-20-5-2-5-3.smt2 diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 53559d949..dfd82b960 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -889,6 +889,24 @@ Node TheoryArith::explain(TNode n) { } } +void flattenAnd(Node n, std::vector& out){ + Assert(n.getKind() == kind::AND); + for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){ + Node curr = *i; + if(curr.getKind() == kind::AND){ + flattenAnd(curr, out); + }else{ + out.push_back(curr); + } + } +} + +Node flattenAnd(Node n){ + std::vector out; + flattenAnd(n, out); + return NodeManager::currentNM()->mkNode(kind::AND, out); +} + void TheoryArith::propagate(Effort e) { if(quickCheckOrMore(e)){ bool propagated = false; @@ -910,8 +928,24 @@ void TheoryArith::propagate(Effort e) { if(flag) { //Currently if the flag is set this came from an equality detected by the //equality engine in the the difference manager. - d_out->propagate(toProp); - propagated = true; + if(toProp.getKind() == kind::EQUAL){ + Node normalized = Rewriter::rewrite(toProp); + Node notNormalized = normalized.notNode(); + + if(d_diseq.find(notNormalized) == d_diseq.end()){ + d_out->propagate(toProp); + propagated = true; + }else{ + Node exp = d_differenceManager.explain(toProp); + Node lp = flattenAnd(exp.andNode(exp)); + d_out->conflict(exp); + propagated = true; + break; + } + }else{ + d_out->propagate(toProp); + propagated = true; + } }else if(inContextAtom(atom)){ Node satValue = d_valuation.getSatValue(toProp); AlwaysAssert(satValue.isNull()); diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am index d7acfb233..0efdf345f 100644 --- a/test/regress/regress1/Makefile.am +++ b/test/regress/regress1/Makefile.am @@ -17,8 +17,12 @@ TESTS = bug136.smt \ hole7.cvc \ hole8.cvc \ instance_1444.smt \ - xs-11-20-5-2-5-3.smt \ - fuzz_2.smt + fuzz_2.smt \ + hash_sat_10_09.smt2 \ + hash_sat_07_17.smt2 \ + ooo.tag10.smt2 \ + hash_sat_06_19.smt2 \ + hash_sat_09_09.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress1/hash_sat_06_19.smt2 b/test/regress/regress1/hash_sat_06_19.smt2 new file mode 100644 index 000000000..b565a4b57 --- /dev/null +++ b/test/regress/regress1/hash_sat_06_19.smt2 @@ -0,0 +1,33 @@ +(set-logic QF_UFLIA) +(set-info :source | MathSat group |) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun hash_1 (Int) Int) +(declare-fun hash_2 (Int) Int) +(declare-fun hash_3 (Int) Int) +(declare-fun hash_4 (Int) Int) +(declare-fun hash_5 (Int) Int) +(declare-fun hash_6 (Int) Int) +(declare-fun hash_7 (Int) Int) +(declare-fun hash_8 (Int) Int) +(declare-fun hash_9 (Int) Int) +(declare-fun hash_10 (Int) Int) +(declare-fun hash_11 (Int) Int) +(declare-fun hash_12 (Int) Int) +(declare-fun hash_13 (Int) Int) +(declare-fun hash_14 (Int) Int) +(declare-fun hash_15 (Int) Int) +(declare-fun hash_16 (Int) Int) +(declare-fun hash_17 (Int) Int) +(declare-fun hash_18 (Int) Int) +(declare-fun hash_19 (Int) Int) +(declare-fun x1 () Int) +(declare-fun x2 () Int) +(declare-fun x3 () Int) +(declare-fun x4 () Int) +(declare-fun x5 () Int) +(declare-fun x6 () Int) +(assert (let ((?v_0 (hash_1 x1)) (?v_1 (hash_1 x2)) (?v_2 (hash_1 x3)) (?v_3 (hash_1 x4)) (?v_4 (hash_1 x5)) (?v_5 (hash_1 x6)) (?v_6 (hash_2 x1)) (?v_7 (hash_2 x2)) (?v_8 (hash_2 x3)) (?v_9 (hash_2 x4)) (?v_10 (hash_2 x5)) (?v_11 (hash_2 x6)) (?v_12 (hash_3 x1)) (?v_13 (hash_3 x2)) (?v_14 (hash_3 x3)) (?v_15 (hash_3 x4)) (?v_16 (hash_3 x5)) (?v_17 (hash_3 x6)) (?v_18 (hash_4 x1)) (?v_19 (hash_4 x2)) (?v_20 (hash_4 x3)) (?v_21 (hash_4 x4)) (?v_22 (hash_4 x5)) (?v_23 (hash_4 x6)) (?v_24 (hash_5 x1)) (?v_25 (hash_5 x2)) (?v_26 (hash_5 x3)) (?v_27 (hash_5 x4)) (?v_28 (hash_5 x5)) (?v_29 (hash_5 x6)) (?v_30 (hash_6 x1)) (?v_31 (hash_6 x2)) (?v_32 (hash_6 x3)) (?v_33 (hash_6 x4)) (?v_34 (hash_6 x5)) (?v_35 (hash_6 x6)) (?v_36 (hash_7 x1)) (?v_37 (hash_7 x2)) (?v_38 (hash_7 x3)) (?v_39 (hash_7 x4)) (?v_40 (hash_7 x5)) (?v_41 (hash_7 x6)) (?v_42 (hash_8 x1)) (?v_43 (hash_8 x2)) (?v_44 (hash_8 x3)) (?v_45 (hash_8 x4)) (?v_46 (hash_8 x5)) (?v_47 (hash_8 x6)) (?v_48 (hash_9 x1)) (?v_49 (hash_9 x2)) (?v_50 (hash_9 x3)) (?v_51 (hash_9 x4)) (?v_52 (hash_9 x5)) (?v_53 (hash_9 x6)) (?v_54 (hash_10 x1)) (?v_55 (hash_10 x2)) (?v_56 (hash_10 x3)) (?v_57 (hash_10 x4)) (?v_58 (hash_10 x5)) (?v_59 (hash_10 x6)) (?v_60 (hash_11 x1)) (?v_61 (hash_11 x2)) (?v_62 (hash_11 x3)) (?v_63 (hash_11 x4)) (?v_64 (hash_11 x5)) (?v_65 (hash_11 x6)) (?v_66 (hash_12 x1)) (?v_67 (hash_12 x2)) (?v_68 (hash_12 x3)) (?v_69 (hash_12 x4)) (?v_70 (hash_12 x5)) (?v_71 (hash_12 x6)) (?v_72 (hash_13 x1)) (?v_73 (hash_13 x2)) (?v_74 (hash_13 x3)) (?v_75 (hash_13 x4)) (?v_76 (hash_13 x5)) (?v_77 (hash_13 x6)) (?v_78 (hash_14 x1)) (?v_79 (hash_14 x2)) (?v_80 (hash_14 x3)) (?v_81 (hash_14 x4)) (?v_82 (hash_14 x5)) (?v_83 (hash_14 x6)) (?v_84 (hash_15 x1)) (?v_85 (hash_15 x2)) (?v_86 (hash_15 x3)) (?v_87 (hash_15 x4)) (?v_88 (hash_15 x5)) (?v_89 (hash_15 x6)) (?v_90 (hash_16 x1)) (?v_91 (hash_16 x2)) (?v_92 (hash_16 x3)) (?v_93 (hash_16 x4)) (?v_94 (hash_16 x5)) (?v_95 (hash_16 x6)) (?v_96 (hash_17 x1)) (?v_97 (hash_17 x2)) (?v_98 (hash_17 x3)) (?v_99 (hash_17 x4)) (?v_100 (hash_17 x5)) (?v_101 (hash_17 x6)) (?v_102 (hash_18 x1)) (?v_103 (hash_18 x2)) (?v_104 (hash_18 x3)) (?v_105 (hash_18 x4)) (?v_106 (hash_18 x5)) (?v_107 (hash_18 x6)) (?v_108 (hash_19 x1)) (?v_109 (hash_19 x2)) (?v_110 (hash_19 x3)) (?v_111 (hash_19 x4)) (?v_112 (hash_19 x5)) (?v_113 (hash_19 x6)) (?v_114 (+ x1 x6)) (?v_115 (+ x1 x2))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (distinct ?v_0 ?v_1) (distinct ?v_0 ?v_2)) (distinct ?v_0 ?v_3)) (distinct ?v_0 ?v_4)) (distinct ?v_0 ?v_5)) (distinct ?v_1 ?v_2)) (distinct ?v_1 ?v_3)) (distinct ?v_1 ?v_4)) (distinct ?v_1 ?v_5)) (distinct ?v_2 ?v_3)) (distinct ?v_2 ?v_4)) (distinct ?v_2 ?v_5)) (distinct ?v_3 ?v_4)) (distinct ?v_3 ?v_5)) (distinct ?v_4 ?v_5)) (distinct ?v_6 ?v_7)) (distinct ?v_6 ?v_8)) (distinct ?v_6 ?v_9)) (distinct ?v_6 ?v_10)) (distinct ?v_6 ?v_11)) (distinct ?v_7 ?v_8)) (distinct ?v_7 ?v_9)) (distinct ?v_7 ?v_10)) (distinct ?v_7 ?v_11)) (distinct ?v_8 ?v_9)) (distinct ?v_8 ?v_10)) (distinct ?v_8 ?v_11)) (distinct ?v_9 ?v_10)) (distinct ?v_9 ?v_11)) (distinct ?v_10 ?v_11)) (distinct ?v_12 ?v_13)) (distinct ?v_12 ?v_14)) (distinct ?v_12 ?v_15)) (distinct ?v_12 ?v_16)) (distinct ?v_12 ?v_17)) (distinct ?v_13 ?v_14)) (distinct ?v_13 ?v_15)) (distinct ?v_13 ?v_16)) (distinct ?v_13 ?v_17)) (distinct ?v_14 ?v_15)) (distinct ?v_14 ?v_16)) (distinct ?v_14 ?v_17)) (distinct ?v_15 ?v_16)) (distinct ?v_15 ?v_17)) (distinct ?v_16 ?v_17)) (distinct ?v_18 ?v_19)) (distinct ?v_18 ?v_20)) (distinct ?v_18 ?v_21)) (distinct ?v_18 ?v_22)) (distinct ?v_18 ?v_23)) (distinct ?v_19 ?v_20)) (distinct ?v_19 ?v_21)) (distinct ?v_19 ?v_22)) (distinct ?v_19 ?v_23)) (distinct ?v_20 ?v_21)) (distinct ?v_20 ?v_22)) (distinct ?v_20 ?v_23)) (distinct ?v_21 ?v_22)) (distinct ?v_21 ?v_23)) (distinct ?v_22 ?v_23)) (distinct ?v_24 ?v_25)) (distinct ?v_24 ?v_26)) (distinct ?v_24 ?v_27)) (distinct ?v_24 ?v_28)) (distinct ?v_24 ?v_29)) (distinct ?v_25 ?v_26)) (distinct ?v_25 ?v_27)) (distinct ?v_25 ?v_28)) (distinct ?v_25 ?v_29)) (distinct ?v_26 ?v_27)) (distinct ?v_26 ?v_28)) (distinct ?v_26 ?v_29)) (distinct ?v_27 ?v_28)) (distinct ?v_27 ?v_29)) (distinct ?v_28 ?v_29)) (distinct ?v_30 ?v_31)) (distinct ?v_30 ?v_32)) (distinct ?v_30 ?v_33)) (distinct ?v_30 ?v_34)) (distinct ?v_30 ?v_35)) (distinct ?v_31 ?v_32)) (distinct ?v_31 ?v_33)) (distinct ?v_31 ?v_34)) (distinct ?v_31 ?v_35)) (distinct ?v_32 ?v_33)) (distinct ?v_32 ?v_34)) (distinct ?v_32 ?v_35)) (distinct ?v_33 ?v_34)) (distinct ?v_33 ?v_35)) (distinct ?v_34 ?v_35)) (distinct ?v_36 ?v_37)) (distinct ?v_36 ?v_38)) (distinct ?v_36 ?v_39)) (distinct ?v_36 ?v_40)) (distinct ?v_36 ?v_41)) (distinct ?v_37 ?v_38)) (distinct ?v_37 ?v_39)) (distinct ?v_37 ?v_40)) (distinct ?v_37 ?v_41)) (distinct ?v_38 ?v_39)) (distinct ?v_38 ?v_40)) (distinct ?v_38 ?v_41)) (distinct ?v_39 ?v_40)) (distinct ?v_39 ?v_41)) (distinct ?v_40 ?v_41)) (distinct ?v_42 ?v_43)) (distinct ?v_42 ?v_44)) (distinct ?v_42 ?v_45)) (distinct ?v_42 ?v_46)) (distinct ?v_42 ?v_47)) (distinct ?v_43 ?v_44)) (distinct ?v_43 ?v_45)) (distinct ?v_43 ?v_46)) (distinct ?v_43 ?v_47)) (distinct ?v_44 ?v_45)) (distinct ?v_44 ?v_46)) (distinct ?v_44 ?v_47)) (distinct ?v_45 ?v_46)) (distinct ?v_45 ?v_47)) (distinct ?v_46 ?v_47)) (distinct ?v_48 ?v_49)) (distinct ?v_48 ?v_50)) (distinct ?v_48 ?v_51)) (distinct ?v_48 ?v_52)) (distinct ?v_48 ?v_53)) (distinct ?v_49 ?v_50)) (distinct ?v_49 ?v_51)) (distinct ?v_49 ?v_52)) (distinct ?v_49 ?v_53)) (distinct ?v_50 ?v_51)) (distinct ?v_50 ?v_52)) (distinct ?v_50 ?v_53)) (distinct ?v_51 ?v_52)) (distinct ?v_51 ?v_53)) (distinct ?v_52 ?v_53)) (distinct ?v_54 ?v_55)) (distinct ?v_54 ?v_56)) (distinct ?v_54 ?v_57)) (distinct ?v_54 ?v_58)) (distinct ?v_54 ?v_59)) (distinct ?v_55 ?v_56)) (distinct ?v_55 ?v_57)) (distinct ?v_55 ?v_58)) (distinct ?v_55 ?v_59)) (distinct ?v_56 ?v_57)) (distinct ?v_56 ?v_58)) (distinct ?v_56 ?v_59)) (distinct ?v_57 ?v_58)) (distinct ?v_57 ?v_59)) (distinct ?v_58 ?v_59)) (distinct ?v_60 ?v_61)) (distinct ?v_60 ?v_62)) (distinct ?v_60 ?v_63)) (distinct ?v_60 ?v_64)) (distinct ?v_60 ?v_65)) (distinct ?v_61 ?v_62)) (distinct ?v_61 ?v_63)) (distinct ?v_61 ?v_64)) (distinct ?v_61 ?v_65)) (distinct ?v_62 ?v_63)) (distinct ?v_62 ?v_64)) (distinct ?v_62 ?v_65)) (distinct ?v_63 ?v_64)) (distinct ?v_63 ?v_65)) (distinct ?v_64 ?v_65)) (distinct ?v_66 ?v_67)) (distinct ?v_66 ?v_68)) (distinct ?v_66 ?v_69)) (distinct ?v_66 ?v_70)) (distinct ?v_66 ?v_71)) (distinct ?v_67 ?v_68)) (distinct ?v_67 ?v_69)) (distinct ?v_67 ?v_70)) (distinct ?v_67 ?v_71)) (distinct ?v_68 ?v_69)) (distinct ?v_68 ?v_70)) (distinct ?v_68 ?v_71)) (distinct ?v_69 ?v_70)) (distinct ?v_69 ?v_71)) (distinct ?v_70 ?v_71)) (distinct ?v_72 ?v_73)) (distinct ?v_72 ?v_74)) (distinct ?v_72 ?v_75)) (distinct ?v_72 ?v_76)) (distinct ?v_72 ?v_77)) (distinct ?v_73 ?v_74)) (distinct ?v_73 ?v_75)) (distinct ?v_73 ?v_76)) (distinct ?v_73 ?v_77)) (distinct ?v_74 ?v_75)) (distinct ?v_74 ?v_76)) (distinct ?v_74 ?v_77)) (distinct ?v_75 ?v_76)) (distinct ?v_75 ?v_77)) (distinct ?v_76 ?v_77)) (distinct ?v_78 ?v_79)) (distinct ?v_78 ?v_80)) (distinct ?v_78 ?v_81)) (distinct ?v_78 ?v_82)) (distinct ?v_78 ?v_83)) (distinct ?v_79 ?v_80)) (distinct ?v_79 ?v_81)) (distinct ?v_79 ?v_82)) (distinct ?v_79 ?v_83)) (distinct ?v_80 ?v_81)) (distinct ?v_80 ?v_82)) (distinct ?v_80 ?v_83)) (distinct ?v_81 ?v_82)) (distinct ?v_81 ?v_83)) (distinct ?v_82 ?v_83)) (distinct ?v_84 ?v_85)) (distinct ?v_84 ?v_86)) (distinct ?v_84 ?v_87)) (distinct ?v_84 ?v_88)) (distinct ?v_84 ?v_89)) (distinct ?v_85 ?v_86)) (distinct ?v_85 ?v_87)) (distinct ?v_85 ?v_88)) (distinct ?v_85 ?v_89)) (distinct ?v_86 ?v_87)) (distinct ?v_86 ?v_88)) (distinct ?v_86 ?v_89)) (distinct ?v_87 ?v_88)) (distinct ?v_87 ?v_89)) (distinct ?v_88 ?v_89)) (distinct ?v_90 ?v_91)) (distinct ?v_90 ?v_92)) (distinct ?v_90 ?v_93)) (distinct ?v_90 ?v_94)) (distinct ?v_90 ?v_95)) (distinct ?v_91 ?v_92)) (distinct ?v_91 ?v_93)) (distinct ?v_91 ?v_94)) (distinct ?v_91 ?v_95)) (distinct ?v_92 ?v_93)) (distinct ?v_92 ?v_94)) (distinct ?v_92 ?v_95)) (distinct ?v_93 ?v_94)) (distinct ?v_93 ?v_95)) (distinct ?v_94 ?v_95)) (distinct ?v_96 ?v_97)) (distinct ?v_96 ?v_98)) (distinct ?v_96 ?v_99)) (distinct ?v_96 ?v_100)) (distinct ?v_96 ?v_101)) (distinct ?v_97 ?v_98)) (distinct ?v_97 ?v_99)) (distinct ?v_97 ?v_100)) (distinct ?v_97 ?v_101)) (distinct ?v_98 ?v_99)) (distinct ?v_98 ?v_100)) (distinct ?v_98 ?v_101)) (distinct ?v_99 ?v_100)) (distinct ?v_99 ?v_101)) (distinct ?v_100 ?v_101)) (distinct ?v_102 ?v_103)) (distinct ?v_102 ?v_104)) (distinct ?v_102 ?v_105)) (distinct ?v_102 ?v_106)) (distinct ?v_102 ?v_107)) (distinct ?v_103 ?v_104)) (distinct ?v_103 ?v_105)) (distinct ?v_103 ?v_106)) (distinct ?v_103 ?v_107)) (distinct ?v_104 ?v_105)) (distinct ?v_104 ?v_106)) (distinct ?v_104 ?v_107)) (distinct ?v_105 ?v_106)) (distinct ?v_105 ?v_107)) (distinct ?v_106 ?v_107)) (distinct ?v_108 ?v_109)) (distinct ?v_108 ?v_110)) (distinct ?v_108 ?v_111)) (distinct ?v_108 ?v_112)) (distinct ?v_108 ?v_113)) (distinct ?v_109 ?v_110)) (distinct ?v_109 ?v_111)) (distinct ?v_109 ?v_112)) (distinct ?v_109 ?v_113)) (distinct ?v_110 ?v_111)) (distinct ?v_110 ?v_112)) (distinct ?v_110 ?v_113)) (distinct ?v_111 ?v_112)) (distinct ?v_111 ?v_113)) (distinct ?v_112 ?v_113)) (or (or (or (or (or (= ?v_0 x1) (= ?v_0 x2)) (= ?v_0 x3)) (= ?v_0 x4)) (= ?v_0 x5)) (= ?v_0 x6))) (or (or (or (or (or (= ?v_1 x1) (= ?v_1 x2)) (= ?v_1 x3)) (= ?v_1 x4)) (= ?v_1 x5)) (= ?v_1 x6))) (or (or (or (or (or (= ?v_2 x1) (= ?v_2 x2)) (= ?v_2 x3)) (= ?v_2 x4)) (= ?v_2 x5)) (= ?v_2 x6))) (or (or (or (or (or (= ?v_3 x1) (= ?v_3 x2)) (= ?v_3 x3)) (= ?v_3 x4)) (= ?v_3 x5)) (= ?v_3 x6))) (or (or (or (or (or (= ?v_4 x1) (= ?v_4 x2)) (= ?v_4 x3)) (= ?v_4 x4)) (= ?v_4 x5)) (= ?v_4 x6))) (or (or (or (or (or (= ?v_5 x1) (= ?v_5 x2)) (= ?v_5 x3)) (= ?v_5 x4)) (= ?v_5 x5)) (= ?v_5 x6))) (or (or (or (or (or (= ?v_6 x1) (= ?v_6 x2)) (= ?v_6 x3)) (= ?v_6 x4)) (= ?v_6 x5)) (= ?v_6 x6))) (or (or (or (or (or (= ?v_7 x1) (= ?v_7 x2)) (= ?v_7 x3)) (= ?v_7 x4)) (= ?v_7 x5)) (= ?v_7 x6))) (or (or (or (or (or (= ?v_8 x1) (= ?v_8 x2)) (= ?v_8 x3)) (= ?v_8 x4)) (= ?v_8 x5)) (= ?v_8 x6))) (or (or (or (or (or (= ?v_9 x1) (= ?v_9 x2)) (= ?v_9 x3)) (= ?v_9 x4)) (= ?v_9 x5)) (= ?v_9 x6))) (or (or (or (or (or (= ?v_10 x1) (= ?v_10 x2)) (= ?v_10 x3)) (= ?v_10 x4)) (= ?v_10 x5)) (= ?v_10 x6))) (or (or (or (or (or (= ?v_11 x1) (= ?v_11 x2)) (= ?v_11 x3)) (= ?v_11 x4)) (= ?v_11 x5)) (= ?v_11 x6))) (or (or (or (or (or (= ?v_12 x1) (= ?v_12 x2)) (= ?v_12 x3)) (= ?v_12 x4)) (= ?v_12 x5)) (= ?v_12 x6))) (or (or (or (or (or (= ?v_13 x1) (= ?v_13 x2)) (= ?v_13 x3)) (= ?v_13 x4)) (= ?v_13 x5)) (= ?v_13 x6))) (or (or (or (or (or (= ?v_14 x1) (= ?v_14 x2)) (= ?v_14 x3)) (= ?v_14 x4)) (= ?v_14 x5)) (= ?v_14 x6))) (or (or (or (or (or (= ?v_15 x1) (= ?v_15 x2)) (= ?v_15 x3)) (= ?v_15 x4)) (= ?v_15 x5)) (= ?v_15 x6))) (or (or (or (or (or (= ?v_16 x1) (= ?v_16 x2)) (= ?v_16 x3)) (= ?v_16 x4)) (= ?v_16 x5)) (= ?v_16 x6))) (or (or (or (or (or (= ?v_17 x1) (= ?v_17 x2)) (= ?v_17 x3)) (= ?v_17 x4)) (= ?v_17 x5)) (= ?v_17 x6))) (or (or (or (or (or (= ?v_18 x1) (= ?v_18 x2)) (= ?v_18 x3)) (= ?v_18 x4)) (= ?v_18 x5)) (= ?v_18 x6))) (or (or (or (or (or (= ?v_19 x1) (= ?v_19 x2)) (= ?v_19 x3)) (= ?v_19 x4)) (= ?v_19 x5)) (= ?v_19 x6))) (or (or (or (or (or (= ?v_20 x1) (= ?v_20 x2)) (= ?v_20 x3)) (= ?v_20 x4)) (= ?v_20 x5)) (= ?v_20 x6))) (or (or (or (or (or (= ?v_21 x1) (= ?v_21 x2)) (= ?v_21 x3)) (= ?v_21 x4)) (= ?v_21 x5)) (= ?v_21 x6))) (or (or (or (or (or (= ?v_22 x1) (= ?v_22 x2)) (= ?v_22 x3)) (= ?v_22 x4)) (= ?v_22 x5)) (= ?v_22 x6))) (or (or (or (or (or (= ?v_23 x1) (= ?v_23 x2)) (= ?v_23 x3)) (= ?v_23 x4)) (= ?v_23 x5)) (= ?v_23 x6))) (or (or (or (or (or (= ?v_24 x1) (= ?v_24 x2)) (= ?v_24 x3)) (= ?v_24 x4)) (= ?v_24 x5)) (= ?v_24 x6))) (or (or (or (or (or (= ?v_25 x1) (= ?v_25 x2)) (= ?v_25 x3)) (= ?v_25 x4)) (= ?v_25 x5)) (= ?v_25 x6))) (or (or (or (or (or (= ?v_26 x1) (= ?v_26 x2)) (= ?v_26 x3)) (= ?v_26 x4)) (= ?v_26 x5)) (= ?v_26 x6))) (or (or (or (or (or (= ?v_27 x1) (= ?v_27 x2)) (= ?v_27 x3)) (= ?v_27 x4)) (= ?v_27 x5)) (= ?v_27 x6))) (or (or (or (or (or (= ?v_28 x1) (= ?v_28 x2)) (= ?v_28 x3)) (= ?v_28 x4)) (= ?v_28 x5)) (= ?v_28 x6))) (or (or (or (or (or (= ?v_29 x1) (= ?v_29 x2)) (= ?v_29 x3)) (= ?v_29 x4)) (= ?v_29 x5)) (= ?v_29 x6))) (or (or (or (or (or (= ?v_30 x1) (= ?v_30 x2)) (= ?v_30 x3)) (= ?v_30 x4)) (= ?v_30 x5)) (= ?v_30 x6))) (or (or (or (or (or (= ?v_31 x1) (= ?v_31 x2)) (= ?v_31 x3)) (= ?v_31 x4)) (= ?v_31 x5)) (= ?v_31 x6))) (or (or (or (or (or (= ?v_32 x1) (= ?v_32 x2)) (= ?v_32 x3)) (= ?v_32 x4)) (= ?v_32 x5)) (= ?v_32 x6))) (or (or (or (or (or (= ?v_33 x1) (= ?v_33 x2)) (= ?v_33 x3)) (= ?v_33 x4)) (= ?v_33 x5)) (= ?v_33 x6))) (or (or (or (or (or (= ?v_34 x1) (= ?v_34 x2)) (= ?v_34 x3)) (= ?v_34 x4)) (= ?v_34 x5)) (= ?v_34 x6))) (or (or (or (or (or (= ?v_35 x1) (= ?v_35 x2)) (= ?v_35 x3)) (= ?v_35 x4)) (= ?v_35 x5)) (= ?v_35 x6))) (or (or (or (or (or (= ?v_36 x1) (= ?v_36 x2)) (= ?v_36 x3)) (= ?v_36 x4)) (= ?v_36 x5)) (= ?v_36 x6))) (or (or (or (or (or (= ?v_37 x1) (= ?v_37 x2)) (= ?v_37 x3)) (= ?v_37 x4)) (= ?v_37 x5)) (= ?v_37 x6))) (or (or (or (or (or (= ?v_38 x1) (= ?v_38 x2)) (= ?v_38 x3)) (= ?v_38 x4)) (= ?v_38 x5)) (= ?v_38 x6))) (or (or (or (or (or (= ?v_39 x1) (= ?v_39 x2)) (= ?v_39 x3)) (= ?v_39 x4)) (= ?v_39 x5)) (= ?v_39 x6))) (or (or (or (or (or (= ?v_40 x1) (= ?v_40 x2)) (= ?v_40 x3)) (= ?v_40 x4)) (= ?v_40 x5)) (= ?v_40 x6))) (or (or (or (or (or (= ?v_41 x1) (= ?v_41 x2)) (= ?v_41 x3)) (= ?v_41 x4)) (= ?v_41 x5)) (= ?v_41 x6))) (or (or (or (or (or (= ?v_42 x1) (= ?v_42 x2)) (= ?v_42 x3)) (= ?v_42 x4)) (= ?v_42 x5)) (= ?v_42 x6))) (or (or (or (or (or (= ?v_43 x1) (= ?v_43 x2)) (= ?v_43 x3)) (= ?v_43 x4)) (= ?v_43 x5)) (= ?v_43 x6))) (or (or (or (or (or (= ?v_44 x1) (= ?v_44 x2)) (= ?v_44 x3)) (= ?v_44 x4)) (= ?v_44 x5)) (= ?v_44 x6))) (or (or (or (or (or (= ?v_45 x1) (= ?v_45 x2)) (= ?v_45 x3)) (= ?v_45 x4)) (= ?v_45 x5)) (= ?v_45 x6))) (or (or (or (or (or (= ?v_46 x1) (= ?v_46 x2)) (= ?v_46 x3)) (= ?v_46 x4)) (= ?v_46 x5)) (= ?v_46 x6))) (or (or (or (or (or (= ?v_47 x1) (= ?v_47 x2)) (= ?v_47 x3)) (= ?v_47 x4)) (= ?v_47 x5)) (= ?v_47 x6))) (or (or (or (or (or (= ?v_48 x1) (= ?v_48 x2)) (= ?v_48 x3)) (= ?v_48 x4)) (= ?v_48 x5)) (= ?v_48 x6))) (or (or (or (or (or (= ?v_49 x1) (= ?v_49 x2)) (= ?v_49 x3)) (= ?v_49 x4)) (= ?v_49 x5)) (= ?v_49 x6))) (or (or (or (or (or (= ?v_50 x1) (= ?v_50 x2)) (= ?v_50 x3)) (= ?v_50 x4)) (= ?v_50 x5)) (= ?v_50 x6))) (or (or (or (or (or (= ?v_51 x1) (= ?v_51 x2)) (= ?v_51 x3)) (= ?v_51 x4)) (= ?v_51 x5)) (= ?v_51 x6))) (or (or (or (or (or (= ?v_52 x1) (= ?v_52 x2)) (= ?v_52 x3)) (= ?v_52 x4)) (= ?v_52 x5)) (= ?v_52 x6))) (or (or (or (or (or (= ?v_53 x1) (= ?v_53 x2)) (= ?v_53 x3)) (= ?v_53 x4)) (= ?v_53 x5)) (= ?v_53 x6))) (or (or (or (or (or (= ?v_54 x1) (= ?v_54 x2)) (= ?v_54 x3)) (= ?v_54 x4)) (= ?v_54 x5)) (= ?v_54 x6))) (or (or (or (or (or (= ?v_55 x1) (= ?v_55 x2)) (= ?v_55 x3)) (= ?v_55 x4)) (= ?v_55 x5)) (= ?v_55 x6))) (or (or (or (or (or (= ?v_56 x1) (= ?v_56 x2)) (= ?v_56 x3)) (= ?v_56 x4)) (= ?v_56 x5)) (= ?v_56 x6))) (or (or (or (or (or (= ?v_57 x1) (= ?v_57 x2)) (= ?v_57 x3)) (= ?v_57 x4)) (= ?v_57 x5)) (= ?v_57 x6))) (or (or (or (or (or (= ?v_58 x1) (= ?v_58 x2)) (= ?v_58 x3)) (= ?v_58 x4)) (= ?v_58 x5)) (= ?v_58 x6))) (or (or (or (or (or (= ?v_59 x1) (= ?v_59 x2)) (= ?v_59 x3)) (= ?v_59 x4)) (= ?v_59 x5)) (= ?v_59 x6))) (or (or (or (or (or (= ?v_60 x1) (= ?v_60 x2)) (= ?v_60 x3)) (= ?v_60 x4)) (= ?v_60 x5)) (= ?v_60 x6))) (or (or (or (or (or (= ?v_61 x1) (= ?v_61 x2)) (= ?v_61 x3)) (= ?v_61 x4)) (= ?v_61 x5)) (= ?v_61 x6))) (or (or (or (or (or (= ?v_62 x1) (= ?v_62 x2)) (= ?v_62 x3)) (= ?v_62 x4)) (= ?v_62 x5)) (= ?v_62 x6))) (or (or (or (or (or (= ?v_63 x1) (= ?v_63 x2)) (= ?v_63 x3)) (= ?v_63 x4)) (= ?v_63 x5)) (= ?v_63 x6))) (or (or (or (or (or (= ?v_64 x1) (= ?v_64 x2)) (= ?v_64 x3)) (= ?v_64 x4)) (= ?v_64 x5)) (= ?v_64 x6))) (or (or (or (or (or (= ?v_65 x1) (= ?v_65 x2)) (= ?v_65 x3)) (= ?v_65 x4)) (= ?v_65 x5)) (= ?v_65 x6))) (or (or (or (or (or (= ?v_66 x1) (= ?v_66 x2)) (= ?v_66 x3)) (= ?v_66 x4)) (= ?v_66 x5)) (= ?v_66 x6))) (or (or (or (or (or (= ?v_67 x1) (= ?v_67 x2)) (= ?v_67 x3)) (= ?v_67 x4)) (= ?v_67 x5)) (= ?v_67 x6))) (or (or (or (or (or (= ?v_68 x1) (= ?v_68 x2)) (= ?v_68 x3)) (= ?v_68 x4)) (= ?v_68 x5)) (= ?v_68 x6))) (or (or (or (or (or (= ?v_69 x1) (= ?v_69 x2)) (= ?v_69 x3)) (= ?v_69 x4)) (= ?v_69 x5)) (= ?v_69 x6))) (or (or (or (or (or (= ?v_70 x1) (= ?v_70 x2)) (= ?v_70 x3)) (= ?v_70 x4)) (= ?v_70 x5)) (= ?v_70 x6))) (or (or (or (or (or (= ?v_71 x1) (= ?v_71 x2)) (= ?v_71 x3)) (= ?v_71 x4)) (= ?v_71 x5)) (= ?v_71 x6))) (or (or (or (or (or (= ?v_72 x1) (= ?v_72 x2)) (= ?v_72 x3)) (= ?v_72 x4)) (= ?v_72 x5)) (= ?v_72 x6))) (or (or (or (or (or (= ?v_73 x1) (= ?v_73 x2)) (= ?v_73 x3)) (= ?v_73 x4)) (= ?v_73 x5)) (= ?v_73 x6))) (or (or (or (or (or (= ?v_74 x1) (= ?v_74 x2)) (= ?v_74 x3)) (= ?v_74 x4)) (= ?v_74 x5)) (= ?v_74 x6))) (or (or (or (or (or (= ?v_75 x1) (= ?v_75 x2)) (= ?v_75 x3)) (= ?v_75 x4)) (= ?v_75 x5)) (= ?v_75 x6))) (or (or (or (or (or (= ?v_76 x1) (= ?v_76 x2)) (= ?v_76 x3)) (= ?v_76 x4)) (= ?v_76 x5)) (= ?v_76 x6))) (or (or (or (or (or (= ?v_77 x1) (= ?v_77 x2)) (= ?v_77 x3)) (= ?v_77 x4)) (= ?v_77 x5)) (= ?v_77 x6))) (or (or (or (or (or (= ?v_78 x1) (= ?v_78 x2)) (= ?v_78 x3)) (= ?v_78 x4)) (= ?v_78 x5)) (= ?v_78 x6))) (or (or (or (or (or (= ?v_79 x1) (= ?v_79 x2)) (= ?v_79 x3)) (= ?v_79 x4)) (= ?v_79 x5)) (= ?v_79 x6))) (or (or (or (or (or (= ?v_80 x1) (= ?v_80 x2)) (= ?v_80 x3)) (= ?v_80 x4)) (= ?v_80 x5)) (= ?v_80 x6))) (or (or (or (or (or (= ?v_81 x1) (= ?v_81 x2)) (= ?v_81 x3)) (= ?v_81 x4)) (= ?v_81 x5)) (= ?v_81 x6))) (or (or (or (or (or (= ?v_82 x1) (= ?v_82 x2)) (= ?v_82 x3)) (= ?v_82 x4)) (= ?v_82 x5)) (= ?v_82 x6))) (or (or (or (or (or (= ?v_83 x1) (= ?v_83 x2)) (= ?v_83 x3)) (= ?v_83 x4)) (= ?v_83 x5)) (= ?v_83 x6))) (or (or (or (or (or (= ?v_84 x1) (= ?v_84 x2)) (= ?v_84 x3)) (= ?v_84 x4)) (= ?v_84 x5)) (= ?v_84 x6))) (or (or (or (or (or (= ?v_85 x1) (= ?v_85 x2)) (= ?v_85 x3)) (= ?v_85 x4)) (= ?v_85 x5)) (= ?v_85 x6))) (or (or (or (or (or (= ?v_86 x1) (= ?v_86 x2)) (= ?v_86 x3)) (= ?v_86 x4)) (= ?v_86 x5)) (= ?v_86 x6))) (or (or (or (or (or (= ?v_87 x1) (= ?v_87 x2)) (= ?v_87 x3)) (= ?v_87 x4)) (= ?v_87 x5)) (= ?v_87 x6))) (or (or (or (or (or (= ?v_88 x1) (= ?v_88 x2)) (= ?v_88 x3)) (= ?v_88 x4)) (= ?v_88 x5)) (= ?v_88 x6))) (or (or (or (or (or (= ?v_89 x1) (= ?v_89 x2)) (= ?v_89 x3)) (= ?v_89 x4)) (= ?v_89 x5)) (= ?v_89 x6))) (or (or (or (or (or (= ?v_90 x1) (= ?v_90 x2)) (= ?v_90 x3)) (= ?v_90 x4)) (= ?v_90 x5)) (= ?v_90 x6))) (or (or (or (or (or (= ?v_91 x1) (= ?v_91 x2)) (= ?v_91 x3)) (= ?v_91 x4)) (= ?v_91 x5)) (= ?v_91 x6))) (or (or (or (or (or (= ?v_92 x1) (= ?v_92 x2)) (= ?v_92 x3)) (= ?v_92 x4)) (= ?v_92 x5)) (= ?v_92 x6))) (or (or (or (or (or (= ?v_93 x1) (= ?v_93 x2)) (= ?v_93 x3)) (= ?v_93 x4)) (= ?v_93 x5)) (= ?v_93 x6))) (or (or (or (or (or (= ?v_94 x1) (= ?v_94 x2)) (= ?v_94 x3)) (= ?v_94 x4)) (= ?v_94 x5)) (= ?v_94 x6))) (or (or (or (or (or (= ?v_95 x1) (= ?v_95 x2)) (= ?v_95 x3)) (= ?v_95 x4)) (= ?v_95 x5)) (= ?v_95 x6))) (or (or (or (or (or (= ?v_96 x1) (= ?v_96 x2)) (= ?v_96 x3)) (= ?v_96 x4)) (= ?v_96 x5)) (= ?v_96 x6))) (or (or (or (or (or (= ?v_97 x1) (= ?v_97 x2)) (= ?v_97 x3)) (= ?v_97 x4)) (= ?v_97 x5)) (= ?v_97 x6))) (or (or (or (or (or (= ?v_98 x1) (= ?v_98 x2)) (= ?v_98 x3)) (= ?v_98 x4)) (= ?v_98 x5)) (= ?v_98 x6))) (or (or (or (or (or (= ?v_99 x1) (= ?v_99 x2)) (= ?v_99 x3)) (= ?v_99 x4)) (= ?v_99 x5)) (= ?v_99 x6))) (or (or (or (or (or (= ?v_100 x1) (= ?v_100 x2)) (= ?v_100 x3)) (= ?v_100 x4)) (= ?v_100 x5)) (= ?v_100 x6))) (or (or (or (or (or (= ?v_101 x1) (= ?v_101 x2)) (= ?v_101 x3)) (= ?v_101 x4)) (= ?v_101 x5)) (= ?v_101 x6))) (or (or (or (or (or (= ?v_102 x1) (= ?v_102 x2)) (= ?v_102 x3)) (= ?v_102 x4)) (= ?v_102 x5)) (= ?v_102 x6))) (or (or (or (or (or (= ?v_103 x1) (= ?v_103 x2)) (= ?v_103 x3)) (= ?v_103 x4)) (= ?v_103 x5)) (= ?v_103 x6))) (or (or (or (or (or (= ?v_104 x1) (= ?v_104 x2)) (= ?v_104 x3)) (= ?v_104 x4)) (= ?v_104 x5)) (= ?v_104 x6))) (or (or (or (or (or (= ?v_105 x1) (= ?v_105 x2)) (= ?v_105 x3)) (= ?v_105 x4)) (= ?v_105 x5)) (= ?v_105 x6))) (or (or (or (or (or (= ?v_106 x1) (= ?v_106 x2)) (= ?v_106 x3)) (= ?v_106 x4)) (= ?v_106 x5)) (= ?v_106 x6))) (or (or (or (or (or (= ?v_107 x1) (= ?v_107 x2)) (= ?v_107 x3)) (= ?v_107 x4)) (= ?v_107 x5)) (= ?v_107 x6))) (or (or (or (or (or (= ?v_108 x1) (= ?v_108 x2)) (= ?v_108 x3)) (= ?v_108 x4)) (= ?v_108 x5)) (= ?v_108 x6))) (or (or (or (or (or (= ?v_109 x1) (= ?v_109 x2)) (= ?v_109 x3)) (= ?v_109 x4)) (= ?v_109 x5)) (= ?v_109 x6))) (or (or (or (or (or (= ?v_110 x1) (= ?v_110 x2)) (= ?v_110 x3)) (= ?v_110 x4)) (= ?v_110 x5)) (= ?v_110 x6))) (or (or (or (or (or (= ?v_111 x1) (= ?v_111 x2)) (= ?v_111 x3)) (= ?v_111 x4)) (= ?v_111 x5)) (= ?v_111 x6))) (or (or (or (or (or (= ?v_112 x1) (= ?v_112 x2)) (= ?v_112 x3)) (= ?v_112 x4)) (= ?v_112 x5)) (= ?v_112 x6))) (or (or (or (or (or (= ?v_113 x1) (= ?v_113 x2)) (= ?v_113 x3)) (= ?v_113 x4)) (= ?v_113 x5)) (= ?v_113 x6))) (distinct x1 x2)) (distinct x1 x3)) (distinct x1 x4)) (distinct x1 x5)) (distinct x1 x6)) (distinct x2 x3)) (distinct x2 x4)) (distinct x2 x5)) (distinct x2 x6)) (distinct x3 x4)) (distinct x3 x5)) (distinct x3 x6)) (distinct x4 x5)) (distinct x4 x6)) (distinct x5 x6)) (<= 0 x1)) (< x1 7)) (<= 0 x2)) (< x2 7)) (<= 0 x3)) (< x3 7)) (<= 0 x4)) (< x4 7)) (<= 0 x5)) (< x5 7)) (<= 0 x6)) (< x6 7)) (= (hash_1 (hash_1 (hash_19 (ite (< ?v_114 7) ?v_114 x1)))) (hash_1 (hash_1 (hash_19 (ite (< ?v_115 7) ?v_115 x1)))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/hash_sat_07_17.smt2 b/test/regress/regress1/hash_sat_07_17.smt2 new file mode 100644 index 000000000..0bb49801a --- /dev/null +++ b/test/regress/regress1/hash_sat_07_17.smt2 @@ -0,0 +1,32 @@ +(set-logic QF_UFLIA) +(set-info :source | MathSat group |) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun hash_1 (Int) Int) +(declare-fun hash_2 (Int) Int) +(declare-fun hash_3 (Int) Int) +(declare-fun hash_4 (Int) Int) +(declare-fun hash_5 (Int) Int) +(declare-fun hash_6 (Int) Int) +(declare-fun hash_7 (Int) Int) +(declare-fun hash_8 (Int) Int) +(declare-fun hash_9 (Int) Int) +(declare-fun hash_10 (Int) Int) +(declare-fun hash_11 (Int) Int) +(declare-fun hash_12 (Int) Int) +(declare-fun hash_13 (Int) Int) +(declare-fun hash_14 (Int) Int) +(declare-fun hash_15 (Int) Int) +(declare-fun hash_16 (Int) Int) +(declare-fun hash_17 (Int) Int) +(declare-fun x1 () Int) +(declare-fun x2 () Int) +(declare-fun x3 () Int) +(declare-fun x4 () Int) +(declare-fun x5 () Int) +(declare-fun x6 () Int) +(declare-fun x7 () Int) +(assert (let ((?v_0 (hash_1 x1)) (?v_1 (hash_1 x2)) (?v_2 (hash_1 x3)) (?v_3 (hash_1 x4)) (?v_4 (hash_1 x5)) (?v_5 (hash_1 x6)) (?v_6 (hash_1 x7)) (?v_7 (hash_2 x1)) (?v_8 (hash_2 x2)) (?v_9 (hash_2 x3)) (?v_10 (hash_2 x4)) (?v_11 (hash_2 x5)) (?v_12 (hash_2 x6)) (?v_13 (hash_2 x7)) (?v_14 (hash_3 x1)) (?v_15 (hash_3 x2)) (?v_16 (hash_3 x3)) (?v_17 (hash_3 x4)) (?v_18 (hash_3 x5)) (?v_19 (hash_3 x6)) (?v_20 (hash_3 x7)) (?v_21 (hash_4 x1)) (?v_22 (hash_4 x2)) (?v_23 (hash_4 x3)) (?v_24 (hash_4 x4)) (?v_25 (hash_4 x5)) (?v_26 (hash_4 x6)) (?v_27 (hash_4 x7)) (?v_28 (hash_5 x1)) (?v_29 (hash_5 x2)) (?v_30 (hash_5 x3)) (?v_31 (hash_5 x4)) (?v_32 (hash_5 x5)) (?v_33 (hash_5 x6)) (?v_34 (hash_5 x7)) (?v_35 (hash_6 x1)) (?v_36 (hash_6 x2)) (?v_37 (hash_6 x3)) (?v_38 (hash_6 x4)) (?v_39 (hash_6 x5)) (?v_40 (hash_6 x6)) (?v_41 (hash_6 x7)) (?v_42 (hash_7 x1)) (?v_43 (hash_7 x2)) (?v_44 (hash_7 x3)) (?v_45 (hash_7 x4)) (?v_46 (hash_7 x5)) (?v_47 (hash_7 x6)) (?v_48 (hash_7 x7)) (?v_49 (hash_8 x1)) (?v_50 (hash_8 x2)) (?v_51 (hash_8 x3)) (?v_52 (hash_8 x4)) (?v_53 (hash_8 x5)) (?v_54 (hash_8 x6)) (?v_55 (hash_8 x7)) (?v_56 (hash_9 x1)) (?v_57 (hash_9 x2)) (?v_58 (hash_9 x3)) (?v_59 (hash_9 x4)) (?v_60 (hash_9 x5)) (?v_61 (hash_9 x6)) (?v_62 (hash_9 x7)) (?v_63 (hash_10 x1)) (?v_64 (hash_10 x2)) (?v_65 (hash_10 x3)) (?v_66 (hash_10 x4)) (?v_67 (hash_10 x5)) (?v_68 (hash_10 x6)) (?v_69 (hash_10 x7)) (?v_70 (hash_11 x1)) (?v_71 (hash_11 x2)) (?v_72 (hash_11 x3)) (?v_73 (hash_11 x4)) (?v_74 (hash_11 x5)) (?v_75 (hash_11 x6)) (?v_76 (hash_11 x7)) (?v_77 (hash_12 x1)) (?v_78 (hash_12 x2)) (?v_79 (hash_12 x3)) (?v_80 (hash_12 x4)) (?v_81 (hash_12 x5)) (?v_82 (hash_12 x6)) (?v_83 (hash_12 x7)) (?v_84 (hash_13 x1)) (?v_85 (hash_13 x2)) (?v_86 (hash_13 x3)) (?v_87 (hash_13 x4)) (?v_88 (hash_13 x5)) (?v_89 (hash_13 x6)) (?v_90 (hash_13 x7)) (?v_91 (hash_14 x1)) (?v_92 (hash_14 x2)) (?v_93 (hash_14 x3)) (?v_94 (hash_14 x4)) (?v_95 (hash_14 x5)) (?v_96 (hash_14 x6)) (?v_97 (hash_14 x7)) (?v_98 (hash_15 x1)) (?v_99 (hash_15 x2)) (?v_100 (hash_15 x3)) (?v_101 (hash_15 x4)) (?v_102 (hash_15 x5)) (?v_103 (hash_15 x6)) (?v_104 (hash_15 x7)) (?v_105 (hash_16 x1)) (?v_106 (hash_16 x2)) (?v_107 (hash_16 x3)) (?v_108 (hash_16 x4)) (?v_109 (hash_16 x5)) (?v_110 (hash_16 x6)) (?v_111 (hash_16 x7)) (?v_112 (hash_17 x1)) (?v_113 (hash_17 x2)) (?v_114 (hash_17 x3)) (?v_115 (hash_17 x4)) (?v_116 (hash_17 x5)) (?v_117 (hash_17 x6)) (?v_118 (hash_17 x7)) (?v_119 (+ x1 x7)) (?v_120 (+ x1 x2))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (distinct ?v_0 ?v_1) (distinct ?v_0 ?v_2)) (distinct ?v_0 ?v_3)) (distinct ?v_0 ?v_4)) (distinct ?v_0 ?v_5)) (distinct ?v_0 ?v_6)) (distinct ?v_1 ?v_2)) (distinct ?v_1 ?v_3)) (distinct ?v_1 ?v_4)) (distinct ?v_1 ?v_5)) (distinct ?v_1 ?v_6)) (distinct ?v_2 ?v_3)) (distinct ?v_2 ?v_4)) (distinct ?v_2 ?v_5)) (distinct ?v_2 ?v_6)) (distinct ?v_3 ?v_4)) (distinct ?v_3 ?v_5)) (distinct ?v_3 ?v_6)) (distinct ?v_4 ?v_5)) (distinct ?v_4 ?v_6)) (distinct ?v_5 ?v_6)) (distinct ?v_7 ?v_8)) (distinct ?v_7 ?v_9)) (distinct ?v_7 ?v_10)) (distinct ?v_7 ?v_11)) (distinct ?v_7 ?v_12)) (distinct ?v_7 ?v_13)) (distinct ?v_8 ?v_9)) (distinct ?v_8 ?v_10)) (distinct ?v_8 ?v_11)) (distinct ?v_8 ?v_12)) (distinct ?v_8 ?v_13)) (distinct ?v_9 ?v_10)) (distinct ?v_9 ?v_11)) (distinct ?v_9 ?v_12)) (distinct ?v_9 ?v_13)) (distinct ?v_10 ?v_11)) (distinct ?v_10 ?v_12)) (distinct ?v_10 ?v_13)) (distinct ?v_11 ?v_12)) (distinct ?v_11 ?v_13)) (distinct ?v_12 ?v_13)) (distinct ?v_14 ?v_15)) (distinct ?v_14 ?v_16)) (distinct ?v_14 ?v_17)) (distinct ?v_14 ?v_18)) (distinct ?v_14 ?v_19)) (distinct ?v_14 ?v_20)) (distinct ?v_15 ?v_16)) (distinct ?v_15 ?v_17)) (distinct ?v_15 ?v_18)) (distinct ?v_15 ?v_19)) (distinct ?v_15 ?v_20)) (distinct ?v_16 ?v_17)) (distinct ?v_16 ?v_18)) (distinct ?v_16 ?v_19)) (distinct ?v_16 ?v_20)) (distinct ?v_17 ?v_18)) (distinct ?v_17 ?v_19)) (distinct ?v_17 ?v_20)) (distinct ?v_18 ?v_19)) (distinct ?v_18 ?v_20)) (distinct ?v_19 ?v_20)) (distinct ?v_21 ?v_22)) (distinct ?v_21 ?v_23)) (distinct ?v_21 ?v_24)) (distinct ?v_21 ?v_25)) (distinct ?v_21 ?v_26)) (distinct ?v_21 ?v_27)) (distinct ?v_22 ?v_23)) (distinct ?v_22 ?v_24)) (distinct ?v_22 ?v_25)) (distinct ?v_22 ?v_26)) (distinct ?v_22 ?v_27)) (distinct ?v_23 ?v_24)) (distinct ?v_23 ?v_25)) (distinct ?v_23 ?v_26)) (distinct ?v_23 ?v_27)) (distinct ?v_24 ?v_25)) (distinct ?v_24 ?v_26)) (distinct ?v_24 ?v_27)) (distinct ?v_25 ?v_26)) (distinct ?v_25 ?v_27)) (distinct ?v_26 ?v_27)) (distinct ?v_28 ?v_29)) (distinct ?v_28 ?v_30)) (distinct ?v_28 ?v_31)) (distinct ?v_28 ?v_32)) (distinct ?v_28 ?v_33)) (distinct ?v_28 ?v_34)) (distinct ?v_29 ?v_30)) (distinct ?v_29 ?v_31)) (distinct ?v_29 ?v_32)) (distinct ?v_29 ?v_33)) (distinct ?v_29 ?v_34)) (distinct ?v_30 ?v_31)) (distinct ?v_30 ?v_32)) (distinct ?v_30 ?v_33)) (distinct ?v_30 ?v_34)) (distinct ?v_31 ?v_32)) (distinct ?v_31 ?v_33)) (distinct ?v_31 ?v_34)) (distinct ?v_32 ?v_33)) (distinct ?v_32 ?v_34)) (distinct ?v_33 ?v_34)) (distinct ?v_35 ?v_36)) (distinct ?v_35 ?v_37)) (distinct ?v_35 ?v_38)) (distinct ?v_35 ?v_39)) (distinct ?v_35 ?v_40)) (distinct ?v_35 ?v_41)) (distinct ?v_36 ?v_37)) (distinct ?v_36 ?v_38)) (distinct ?v_36 ?v_39)) (distinct ?v_36 ?v_40)) (distinct ?v_36 ?v_41)) (distinct ?v_37 ?v_38)) (distinct ?v_37 ?v_39)) (distinct ?v_37 ?v_40)) (distinct ?v_37 ?v_41)) (distinct ?v_38 ?v_39)) (distinct ?v_38 ?v_40)) (distinct ?v_38 ?v_41)) (distinct ?v_39 ?v_40)) (distinct ?v_39 ?v_41)) (distinct ?v_40 ?v_41)) (distinct ?v_42 ?v_43)) (distinct ?v_42 ?v_44)) (distinct ?v_42 ?v_45)) (distinct ?v_42 ?v_46)) (distinct ?v_42 ?v_47)) (distinct ?v_42 ?v_48)) (distinct ?v_43 ?v_44)) (distinct ?v_43 ?v_45)) (distinct ?v_43 ?v_46)) (distinct ?v_43 ?v_47)) (distinct ?v_43 ?v_48)) (distinct ?v_44 ?v_45)) (distinct ?v_44 ?v_46)) (distinct ?v_44 ?v_47)) (distinct ?v_44 ?v_48)) (distinct ?v_45 ?v_46)) (distinct ?v_45 ?v_47)) (distinct ?v_45 ?v_48)) (distinct ?v_46 ?v_47)) (distinct ?v_46 ?v_48)) (distinct ?v_47 ?v_48)) (distinct ?v_49 ?v_50)) (distinct ?v_49 ?v_51)) (distinct ?v_49 ?v_52)) (distinct ?v_49 ?v_53)) (distinct ?v_49 ?v_54)) (distinct ?v_49 ?v_55)) (distinct ?v_50 ?v_51)) (distinct ?v_50 ?v_52)) (distinct ?v_50 ?v_53)) (distinct ?v_50 ?v_54)) (distinct ?v_50 ?v_55)) (distinct ?v_51 ?v_52)) (distinct ?v_51 ?v_53)) (distinct ?v_51 ?v_54)) (distinct ?v_51 ?v_55)) (distinct ?v_52 ?v_53)) (distinct ?v_52 ?v_54)) (distinct ?v_52 ?v_55)) (distinct ?v_53 ?v_54)) (distinct ?v_53 ?v_55)) (distinct ?v_54 ?v_55)) (distinct ?v_56 ?v_57)) (distinct ?v_56 ?v_58)) (distinct ?v_56 ?v_59)) (distinct ?v_56 ?v_60)) (distinct ?v_56 ?v_61)) (distinct ?v_56 ?v_62)) (distinct ?v_57 ?v_58)) (distinct ?v_57 ?v_59)) (distinct ?v_57 ?v_60)) (distinct ?v_57 ?v_61)) (distinct ?v_57 ?v_62)) (distinct ?v_58 ?v_59)) (distinct ?v_58 ?v_60)) (distinct ?v_58 ?v_61)) (distinct ?v_58 ?v_62)) (distinct ?v_59 ?v_60)) (distinct ?v_59 ?v_61)) (distinct ?v_59 ?v_62)) (distinct ?v_60 ?v_61)) (distinct ?v_60 ?v_62)) (distinct ?v_61 ?v_62)) (distinct ?v_63 ?v_64)) (distinct ?v_63 ?v_65)) (distinct ?v_63 ?v_66)) (distinct ?v_63 ?v_67)) (distinct ?v_63 ?v_68)) (distinct ?v_63 ?v_69)) (distinct ?v_64 ?v_65)) (distinct ?v_64 ?v_66)) (distinct ?v_64 ?v_67)) (distinct ?v_64 ?v_68)) (distinct ?v_64 ?v_69)) (distinct ?v_65 ?v_66)) (distinct ?v_65 ?v_67)) (distinct ?v_65 ?v_68)) (distinct ?v_65 ?v_69)) (distinct ?v_66 ?v_67)) (distinct ?v_66 ?v_68)) (distinct ?v_66 ?v_69)) (distinct ?v_67 ?v_68)) (distinct ?v_67 ?v_69)) (distinct ?v_68 ?v_69)) (distinct ?v_70 ?v_71)) (distinct ?v_70 ?v_72)) (distinct ?v_70 ?v_73)) (distinct ?v_70 ?v_74)) (distinct ?v_70 ?v_75)) (distinct ?v_70 ?v_76)) (distinct ?v_71 ?v_72)) (distinct ?v_71 ?v_73)) (distinct ?v_71 ?v_74)) (distinct ?v_71 ?v_75)) (distinct ?v_71 ?v_76)) (distinct ?v_72 ?v_73)) (distinct ?v_72 ?v_74)) (distinct ?v_72 ?v_75)) (distinct ?v_72 ?v_76)) (distinct ?v_73 ?v_74)) (distinct ?v_73 ?v_75)) (distinct ?v_73 ?v_76)) (distinct ?v_74 ?v_75)) (distinct ?v_74 ?v_76)) (distinct ?v_75 ?v_76)) (distinct ?v_77 ?v_78)) (distinct ?v_77 ?v_79)) (distinct ?v_77 ?v_80)) (distinct ?v_77 ?v_81)) (distinct ?v_77 ?v_82)) (distinct ?v_77 ?v_83)) (distinct ?v_78 ?v_79)) (distinct ?v_78 ?v_80)) (distinct ?v_78 ?v_81)) (distinct ?v_78 ?v_82)) (distinct ?v_78 ?v_83)) (distinct ?v_79 ?v_80)) (distinct ?v_79 ?v_81)) (distinct ?v_79 ?v_82)) (distinct ?v_79 ?v_83)) (distinct ?v_80 ?v_81)) (distinct ?v_80 ?v_82)) (distinct ?v_80 ?v_83)) (distinct ?v_81 ?v_82)) (distinct ?v_81 ?v_83)) (distinct ?v_82 ?v_83)) (distinct ?v_84 ?v_85)) (distinct ?v_84 ?v_86)) (distinct ?v_84 ?v_87)) (distinct ?v_84 ?v_88)) (distinct ?v_84 ?v_89)) (distinct ?v_84 ?v_90)) (distinct ?v_85 ?v_86)) (distinct ?v_85 ?v_87)) (distinct ?v_85 ?v_88)) (distinct ?v_85 ?v_89)) (distinct ?v_85 ?v_90)) (distinct ?v_86 ?v_87)) (distinct ?v_86 ?v_88)) (distinct ?v_86 ?v_89)) (distinct ?v_86 ?v_90)) (distinct ?v_87 ?v_88)) (distinct ?v_87 ?v_89)) (distinct ?v_87 ?v_90)) (distinct ?v_88 ?v_89)) (distinct ?v_88 ?v_90)) (distinct ?v_89 ?v_90)) (distinct ?v_91 ?v_92)) (distinct ?v_91 ?v_93)) (distinct ?v_91 ?v_94)) (distinct ?v_91 ?v_95)) (distinct ?v_91 ?v_96)) (distinct ?v_91 ?v_97)) (distinct ?v_92 ?v_93)) (distinct ?v_92 ?v_94)) (distinct ?v_92 ?v_95)) (distinct ?v_92 ?v_96)) (distinct ?v_92 ?v_97)) (distinct ?v_93 ?v_94)) (distinct ?v_93 ?v_95)) (distinct ?v_93 ?v_96)) (distinct ?v_93 ?v_97)) (distinct ?v_94 ?v_95)) (distinct ?v_94 ?v_96)) (distinct ?v_94 ?v_97)) (distinct ?v_95 ?v_96)) (distinct ?v_95 ?v_97)) (distinct ?v_96 ?v_97)) (distinct ?v_98 ?v_99)) (distinct ?v_98 ?v_100)) (distinct ?v_98 ?v_101)) (distinct ?v_98 ?v_102)) (distinct ?v_98 ?v_103)) (distinct ?v_98 ?v_104)) (distinct ?v_99 ?v_100)) (distinct ?v_99 ?v_101)) (distinct ?v_99 ?v_102)) (distinct ?v_99 ?v_103)) (distinct ?v_99 ?v_104)) (distinct ?v_100 ?v_101)) (distinct ?v_100 ?v_102)) (distinct ?v_100 ?v_103)) (distinct ?v_100 ?v_104)) (distinct ?v_101 ?v_102)) (distinct ?v_101 ?v_103)) (distinct ?v_101 ?v_104)) (distinct ?v_102 ?v_103)) (distinct ?v_102 ?v_104)) (distinct ?v_103 ?v_104)) (distinct ?v_105 ?v_106)) (distinct ?v_105 ?v_107)) (distinct ?v_105 ?v_108)) (distinct ?v_105 ?v_109)) (distinct ?v_105 ?v_110)) (distinct ?v_105 ?v_111)) (distinct ?v_106 ?v_107)) (distinct ?v_106 ?v_108)) (distinct ?v_106 ?v_109)) (distinct ?v_106 ?v_110)) (distinct ?v_106 ?v_111)) (distinct ?v_107 ?v_108)) (distinct ?v_107 ?v_109)) (distinct ?v_107 ?v_110)) (distinct ?v_107 ?v_111)) (distinct ?v_108 ?v_109)) (distinct ?v_108 ?v_110)) (distinct ?v_108 ?v_111)) (distinct ?v_109 ?v_110)) (distinct ?v_109 ?v_111)) (distinct ?v_110 ?v_111)) (distinct ?v_112 ?v_113)) (distinct ?v_112 ?v_114)) (distinct ?v_112 ?v_115)) (distinct ?v_112 ?v_116)) (distinct ?v_112 ?v_117)) (distinct ?v_112 ?v_118)) (distinct ?v_113 ?v_114)) (distinct ?v_113 ?v_115)) (distinct ?v_113 ?v_116)) (distinct ?v_113 ?v_117)) (distinct ?v_113 ?v_118)) (distinct ?v_114 ?v_115)) (distinct ?v_114 ?v_116)) (distinct ?v_114 ?v_117)) (distinct ?v_114 ?v_118)) (distinct ?v_115 ?v_116)) (distinct ?v_115 ?v_117)) (distinct ?v_115 ?v_118)) (distinct ?v_116 ?v_117)) (distinct ?v_116 ?v_118)) (distinct ?v_117 ?v_118)) (or (or (or (or (or (or (= ?v_0 x1) (= ?v_0 x2)) (= ?v_0 x3)) (= ?v_0 x4)) (= ?v_0 x5)) (= ?v_0 x6)) (= ?v_0 x7))) (or (or (or (or (or (or (= ?v_1 x1) (= ?v_1 x2)) (= ?v_1 x3)) (= ?v_1 x4)) (= ?v_1 x5)) (= ?v_1 x6)) (= ?v_1 x7))) (or (or (or (or (or (or (= ?v_2 x1) (= ?v_2 x2)) (= ?v_2 x3)) (= ?v_2 x4)) (= ?v_2 x5)) (= ?v_2 x6)) (= ?v_2 x7))) (or (or (or (or (or (or (= ?v_3 x1) (= ?v_3 x2)) (= ?v_3 x3)) (= ?v_3 x4)) (= ?v_3 x5)) (= ?v_3 x6)) (= ?v_3 x7))) (or (or (or (or (or (or (= ?v_4 x1) (= ?v_4 x2)) (= ?v_4 x3)) (= ?v_4 x4)) (= ?v_4 x5)) (= ?v_4 x6)) (= ?v_4 x7))) (or (or (or (or (or (or (= ?v_5 x1) (= ?v_5 x2)) (= ?v_5 x3)) (= ?v_5 x4)) (= ?v_5 x5)) (= ?v_5 x6)) (= ?v_5 x7))) (or (or (or (or (or (or (= ?v_6 x1) (= ?v_6 x2)) (= ?v_6 x3)) (= ?v_6 x4)) (= ?v_6 x5)) (= ?v_6 x6)) (= ?v_6 x7))) (or (or (or (or (or (or (= ?v_7 x1) (= ?v_7 x2)) (= ?v_7 x3)) (= ?v_7 x4)) (= ?v_7 x5)) (= ?v_7 x6)) (= ?v_7 x7))) (or (or (or (or (or (or (= ?v_8 x1) (= ?v_8 x2)) (= ?v_8 x3)) (= ?v_8 x4)) (= ?v_8 x5)) (= ?v_8 x6)) (= ?v_8 x7))) (or (or (or (or (or (or (= ?v_9 x1) (= ?v_9 x2)) (= ?v_9 x3)) (= ?v_9 x4)) (= ?v_9 x5)) (= ?v_9 x6)) (= ?v_9 x7))) (or (or (or (or (or (or (= ?v_10 x1) (= ?v_10 x2)) (= ?v_10 x3)) (= ?v_10 x4)) (= ?v_10 x5)) (= ?v_10 x6)) (= ?v_10 x7))) (or (or (or (or (or (or (= ?v_11 x1) (= ?v_11 x2)) (= ?v_11 x3)) (= ?v_11 x4)) (= ?v_11 x5)) (= ?v_11 x6)) (= ?v_11 x7))) (or (or (or (or (or (or (= ?v_12 x1) (= ?v_12 x2)) (= ?v_12 x3)) (= ?v_12 x4)) (= ?v_12 x5)) (= ?v_12 x6)) (= ?v_12 x7))) (or (or (or (or (or (or (= ?v_13 x1) (= ?v_13 x2)) (= ?v_13 x3)) (= ?v_13 x4)) (= ?v_13 x5)) (= ?v_13 x6)) (= ?v_13 x7))) (or (or (or (or (or (or (= ?v_14 x1) (= ?v_14 x2)) (= ?v_14 x3)) (= ?v_14 x4)) (= ?v_14 x5)) (= ?v_14 x6)) (= ?v_14 x7))) (or (or (or (or (or (or (= ?v_15 x1) (= ?v_15 x2)) (= ?v_15 x3)) (= ?v_15 x4)) (= ?v_15 x5)) (= ?v_15 x6)) (= ?v_15 x7))) (or (or (or (or (or (or (= ?v_16 x1) (= ?v_16 x2)) (= ?v_16 x3)) (= ?v_16 x4)) (= ?v_16 x5)) (= ?v_16 x6)) (= ?v_16 x7))) (or (or (or (or (or (or (= ?v_17 x1) (= ?v_17 x2)) (= ?v_17 x3)) (= ?v_17 x4)) (= ?v_17 x5)) (= ?v_17 x6)) (= ?v_17 x7))) (or (or (or (or (or (or (= ?v_18 x1) (= ?v_18 x2)) (= ?v_18 x3)) (= ?v_18 x4)) (= ?v_18 x5)) (= ?v_18 x6)) (= ?v_18 x7))) (or (or (or (or (or (or (= ?v_19 x1) (= ?v_19 x2)) (= ?v_19 x3)) (= ?v_19 x4)) (= ?v_19 x5)) (= ?v_19 x6)) (= ?v_19 x7))) (or (or (or (or (or (or (= ?v_20 x1) (= ?v_20 x2)) (= ?v_20 x3)) (= ?v_20 x4)) (= ?v_20 x5)) (= ?v_20 x6)) (= ?v_20 x7))) (or (or (or (or (or (or (= ?v_21 x1) (= ?v_21 x2)) (= ?v_21 x3)) (= ?v_21 x4)) (= ?v_21 x5)) (= ?v_21 x6)) (= ?v_21 x7))) (or (or (or (or (or (or (= ?v_22 x1) (= ?v_22 x2)) (= ?v_22 x3)) (= ?v_22 x4)) (= ?v_22 x5)) (= ?v_22 x6)) (= ?v_22 x7))) (or (or (or (or (or (or (= ?v_23 x1) (= ?v_23 x2)) (= ?v_23 x3)) (= ?v_23 x4)) (= ?v_23 x5)) (= ?v_23 x6)) (= ?v_23 x7))) (or (or (or (or (or (or (= ?v_24 x1) (= ?v_24 x2)) (= ?v_24 x3)) (= ?v_24 x4)) (= ?v_24 x5)) (= ?v_24 x6)) (= ?v_24 x7))) (or (or (or (or (or (or (= ?v_25 x1) (= ?v_25 x2)) (= ?v_25 x3)) (= ?v_25 x4)) (= ?v_25 x5)) (= ?v_25 x6)) (= ?v_25 x7))) (or (or (or (or (or (or (= ?v_26 x1) (= ?v_26 x2)) (= ?v_26 x3)) (= ?v_26 x4)) (= ?v_26 x5)) (= ?v_26 x6)) (= ?v_26 x7))) (or (or (or (or (or (or (= ?v_27 x1) (= ?v_27 x2)) (= ?v_27 x3)) (= ?v_27 x4)) (= ?v_27 x5)) (= ?v_27 x6)) (= ?v_27 x7))) (or (or (or (or (or (or (= ?v_28 x1) (= ?v_28 x2)) (= ?v_28 x3)) (= ?v_28 x4)) (= ?v_28 x5)) (= ?v_28 x6)) (= ?v_28 x7))) (or (or (or (or (or (or (= ?v_29 x1) (= ?v_29 x2)) (= ?v_29 x3)) (= ?v_29 x4)) (= ?v_29 x5)) (= ?v_29 x6)) (= ?v_29 x7))) (or (or (or (or (or (or (= ?v_30 x1) (= ?v_30 x2)) (= ?v_30 x3)) (= ?v_30 x4)) (= ?v_30 x5)) (= ?v_30 x6)) (= ?v_30 x7))) (or (or (or (or (or (or (= ?v_31 x1) (= ?v_31 x2)) (= ?v_31 x3)) (= ?v_31 x4)) (= ?v_31 x5)) (= ?v_31 x6)) (= ?v_31 x7))) (or (or (or (or (or (or (= ?v_32 x1) (= ?v_32 x2)) (= ?v_32 x3)) (= ?v_32 x4)) (= ?v_32 x5)) (= ?v_32 x6)) (= ?v_32 x7))) (or (or (or (or (or (or (= ?v_33 x1) (= ?v_33 x2)) (= ?v_33 x3)) (= ?v_33 x4)) (= ?v_33 x5)) (= ?v_33 x6)) (= ?v_33 x7))) (or (or (or (or (or (or (= ?v_34 x1) (= ?v_34 x2)) (= ?v_34 x3)) (= ?v_34 x4)) (= ?v_34 x5)) (= ?v_34 x6)) (= ?v_34 x7))) (or (or (or (or (or (or (= ?v_35 x1) (= ?v_35 x2)) (= ?v_35 x3)) (= ?v_35 x4)) (= ?v_35 x5)) (= ?v_35 x6)) (= ?v_35 x7))) (or (or (or (or (or (or (= ?v_36 x1) (= ?v_36 x2)) (= ?v_36 x3)) (= ?v_36 x4)) (= ?v_36 x5)) (= ?v_36 x6)) (= ?v_36 x7))) (or (or (or (or (or (or (= ?v_37 x1) (= ?v_37 x2)) (= ?v_37 x3)) (= ?v_37 x4)) (= ?v_37 x5)) (= ?v_37 x6)) (= ?v_37 x7))) (or (or (or (or (or (or (= ?v_38 x1) (= ?v_38 x2)) (= ?v_38 x3)) (= ?v_38 x4)) (= ?v_38 x5)) (= ?v_38 x6)) (= ?v_38 x7))) (or (or (or (or (or (or (= ?v_39 x1) (= ?v_39 x2)) (= ?v_39 x3)) (= ?v_39 x4)) (= ?v_39 x5)) (= ?v_39 x6)) (= ?v_39 x7))) (or (or (or (or (or (or (= ?v_40 x1) (= ?v_40 x2)) (= ?v_40 x3)) (= ?v_40 x4)) (= ?v_40 x5)) (= ?v_40 x6)) (= ?v_40 x7))) (or (or (or (or (or (or (= ?v_41 x1) (= ?v_41 x2)) (= ?v_41 x3)) (= ?v_41 x4)) (= ?v_41 x5)) (= ?v_41 x6)) (= ?v_41 x7))) (or (or (or (or (or (or (= ?v_42 x1) (= ?v_42 x2)) (= ?v_42 x3)) (= ?v_42 x4)) (= ?v_42 x5)) (= ?v_42 x6)) (= ?v_42 x7))) (or (or (or (or (or (or (= ?v_43 x1) (= ?v_43 x2)) (= ?v_43 x3)) (= ?v_43 x4)) (= ?v_43 x5)) (= ?v_43 x6)) (= ?v_43 x7))) (or (or (or (or (or (or (= ?v_44 x1) (= ?v_44 x2)) (= ?v_44 x3)) (= ?v_44 x4)) (= ?v_44 x5)) (= ?v_44 x6)) (= ?v_44 x7))) (or (or (or (or (or (or (= ?v_45 x1) (= ?v_45 x2)) (= ?v_45 x3)) (= ?v_45 x4)) (= ?v_45 x5)) (= ?v_45 x6)) (= ?v_45 x7))) (or (or (or (or (or (or (= ?v_46 x1) (= ?v_46 x2)) (= ?v_46 x3)) (= ?v_46 x4)) (= ?v_46 x5)) (= ?v_46 x6)) (= ?v_46 x7))) (or (or (or (or (or (or (= ?v_47 x1) (= ?v_47 x2)) (= ?v_47 x3)) (= ?v_47 x4)) (= ?v_47 x5)) (= ?v_47 x6)) (= ?v_47 x7))) (or (or (or (or (or (or (= ?v_48 x1) (= ?v_48 x2)) (= ?v_48 x3)) (= ?v_48 x4)) (= ?v_48 x5)) (= ?v_48 x6)) (= ?v_48 x7))) (or (or (or (or (or (or (= ?v_49 x1) (= ?v_49 x2)) (= ?v_49 x3)) (= ?v_49 x4)) (= ?v_49 x5)) (= ?v_49 x6)) (= ?v_49 x7))) (or (or (or (or (or (or (= ?v_50 x1) (= ?v_50 x2)) (= ?v_50 x3)) (= ?v_50 x4)) (= ?v_50 x5)) (= ?v_50 x6)) (= ?v_50 x7))) (or (or (or (or (or (or (= ?v_51 x1) (= ?v_51 x2)) (= ?v_51 x3)) (= ?v_51 x4)) (= ?v_51 x5)) (= ?v_51 x6)) (= ?v_51 x7))) (or (or (or (or (or (or (= ?v_52 x1) (= ?v_52 x2)) (= ?v_52 x3)) (= ?v_52 x4)) (= ?v_52 x5)) (= ?v_52 x6)) (= ?v_52 x7))) (or (or (or (or (or (or (= ?v_53 x1) (= ?v_53 x2)) (= ?v_53 x3)) (= ?v_53 x4)) (= ?v_53 x5)) (= ?v_53 x6)) (= ?v_53 x7))) (or (or (or (or (or (or (= ?v_54 x1) (= ?v_54 x2)) (= ?v_54 x3)) (= ?v_54 x4)) (= ?v_54 x5)) (= ?v_54 x6)) (= ?v_54 x7))) (or (or (or (or (or (or (= ?v_55 x1) (= ?v_55 x2)) (= ?v_55 x3)) (= ?v_55 x4)) (= ?v_55 x5)) (= ?v_55 x6)) (= ?v_55 x7))) (or (or (or (or (or (or (= ?v_56 x1) (= ?v_56 x2)) (= ?v_56 x3)) (= ?v_56 x4)) (= ?v_56 x5)) (= ?v_56 x6)) (= ?v_56 x7))) (or (or (or (or (or (or (= ?v_57 x1) (= ?v_57 x2)) (= ?v_57 x3)) (= ?v_57 x4)) (= ?v_57 x5)) (= ?v_57 x6)) (= ?v_57 x7))) (or (or (or (or (or (or (= ?v_58 x1) (= ?v_58 x2)) (= ?v_58 x3)) (= ?v_58 x4)) (= ?v_58 x5)) (= ?v_58 x6)) (= ?v_58 x7))) (or (or (or (or (or (or (= ?v_59 x1) (= ?v_59 x2)) (= ?v_59 x3)) (= ?v_59 x4)) (= ?v_59 x5)) (= ?v_59 x6)) (= ?v_59 x7))) (or (or (or (or (or (or (= ?v_60 x1) (= ?v_60 x2)) (= ?v_60 x3)) (= ?v_60 x4)) (= ?v_60 x5)) (= ?v_60 x6)) (= ?v_60 x7))) (or (or (or (or (or (or (= ?v_61 x1) (= ?v_61 x2)) (= ?v_61 x3)) (= ?v_61 x4)) (= ?v_61 x5)) (= ?v_61 x6)) (= ?v_61 x7))) (or (or (or (or (or (or (= ?v_62 x1) (= ?v_62 x2)) (= ?v_62 x3)) (= ?v_62 x4)) (= ?v_62 x5)) (= ?v_62 x6)) (= ?v_62 x7))) (or (or (or (or (or (or (= ?v_63 x1) (= ?v_63 x2)) (= ?v_63 x3)) (= ?v_63 x4)) (= ?v_63 x5)) (= ?v_63 x6)) (= ?v_63 x7))) (or (or (or (or (or (or (= ?v_64 x1) (= ?v_64 x2)) (= ?v_64 x3)) (= ?v_64 x4)) (= ?v_64 x5)) (= ?v_64 x6)) (= ?v_64 x7))) (or (or (or (or (or (or (= ?v_65 x1) (= ?v_65 x2)) (= ?v_65 x3)) (= ?v_65 x4)) (= ?v_65 x5)) (= ?v_65 x6)) (= ?v_65 x7))) (or (or (or (or (or (or (= ?v_66 x1) (= ?v_66 x2)) (= ?v_66 x3)) (= ?v_66 x4)) (= ?v_66 x5)) (= ?v_66 x6)) (= ?v_66 x7))) (or (or (or (or (or (or (= ?v_67 x1) (= ?v_67 x2)) (= ?v_67 x3)) (= ?v_67 x4)) (= ?v_67 x5)) (= ?v_67 x6)) (= ?v_67 x7))) (or (or (or (or (or (or (= ?v_68 x1) (= ?v_68 x2)) (= ?v_68 x3)) (= ?v_68 x4)) (= ?v_68 x5)) (= ?v_68 x6)) (= ?v_68 x7))) (or (or (or (or (or (or (= ?v_69 x1) (= ?v_69 x2)) (= ?v_69 x3)) (= ?v_69 x4)) (= ?v_69 x5)) (= ?v_69 x6)) (= ?v_69 x7))) (or (or (or (or (or (or (= ?v_70 x1) (= ?v_70 x2)) (= ?v_70 x3)) (= ?v_70 x4)) (= ?v_70 x5)) (= ?v_70 x6)) (= ?v_70 x7))) (or (or (or (or (or (or (= ?v_71 x1) (= ?v_71 x2)) (= ?v_71 x3)) (= ?v_71 x4)) (= ?v_71 x5)) (= ?v_71 x6)) (= ?v_71 x7))) (or (or (or (or (or (or (= ?v_72 x1) (= ?v_72 x2)) (= ?v_72 x3)) (= ?v_72 x4)) (= ?v_72 x5)) (= ?v_72 x6)) (= ?v_72 x7))) (or (or (or (or (or (or (= ?v_73 x1) (= ?v_73 x2)) (= ?v_73 x3)) (= ?v_73 x4)) (= ?v_73 x5)) (= ?v_73 x6)) (= ?v_73 x7))) (or (or (or (or (or (or (= ?v_74 x1) (= ?v_74 x2)) (= ?v_74 x3)) (= ?v_74 x4)) (= ?v_74 x5)) (= ?v_74 x6)) (= ?v_74 x7))) (or (or (or (or (or (or (= ?v_75 x1) (= ?v_75 x2)) (= ?v_75 x3)) (= ?v_75 x4)) (= ?v_75 x5)) (= ?v_75 x6)) (= ?v_75 x7))) (or (or (or (or (or (or (= ?v_76 x1) (= ?v_76 x2)) (= ?v_76 x3)) (= ?v_76 x4)) (= ?v_76 x5)) (= ?v_76 x6)) (= ?v_76 x7))) (or (or (or (or (or (or (= ?v_77 x1) (= ?v_77 x2)) (= ?v_77 x3)) (= ?v_77 x4)) (= ?v_77 x5)) (= ?v_77 x6)) (= ?v_77 x7))) (or (or (or (or (or (or (= ?v_78 x1) (= ?v_78 x2)) (= ?v_78 x3)) (= ?v_78 x4)) (= ?v_78 x5)) (= ?v_78 x6)) (= ?v_78 x7))) (or (or (or (or (or (or (= ?v_79 x1) (= ?v_79 x2)) (= ?v_79 x3)) (= ?v_79 x4)) (= ?v_79 x5)) (= ?v_79 x6)) (= ?v_79 x7))) (or (or (or (or (or (or (= ?v_80 x1) (= ?v_80 x2)) (= ?v_80 x3)) (= ?v_80 x4)) (= ?v_80 x5)) (= ?v_80 x6)) (= ?v_80 x7))) (or (or (or (or (or (or (= ?v_81 x1) (= ?v_81 x2)) (= ?v_81 x3)) (= ?v_81 x4)) (= ?v_81 x5)) (= ?v_81 x6)) (= ?v_81 x7))) (or (or (or (or (or (or (= ?v_82 x1) (= ?v_82 x2)) (= ?v_82 x3)) (= ?v_82 x4)) (= ?v_82 x5)) (= ?v_82 x6)) (= ?v_82 x7))) (or (or (or (or (or (or (= ?v_83 x1) (= ?v_83 x2)) (= ?v_83 x3)) (= ?v_83 x4)) (= ?v_83 x5)) (= ?v_83 x6)) (= ?v_83 x7))) (or (or (or (or (or (or (= ?v_84 x1) (= ?v_84 x2)) (= ?v_84 x3)) (= ?v_84 x4)) (= ?v_84 x5)) (= ?v_84 x6)) (= ?v_84 x7))) (or (or (or (or (or (or (= ?v_85 x1) (= ?v_85 x2)) (= ?v_85 x3)) (= ?v_85 x4)) (= ?v_85 x5)) (= ?v_85 x6)) (= ?v_85 x7))) (or (or (or (or (or (or (= ?v_86 x1) (= ?v_86 x2)) (= ?v_86 x3)) (= ?v_86 x4)) (= ?v_86 x5)) (= ?v_86 x6)) (= ?v_86 x7))) (or (or (or (or (or (or (= ?v_87 x1) (= ?v_87 x2)) (= ?v_87 x3)) (= ?v_87 x4)) (= ?v_87 x5)) (= ?v_87 x6)) (= ?v_87 x7))) (or (or (or (or (or (or (= ?v_88 x1) (= ?v_88 x2)) (= ?v_88 x3)) (= ?v_88 x4)) (= ?v_88 x5)) (= ?v_88 x6)) (= ?v_88 x7))) (or (or (or (or (or (or (= ?v_89 x1) (= ?v_89 x2)) (= ?v_89 x3)) (= ?v_89 x4)) (= ?v_89 x5)) (= ?v_89 x6)) (= ?v_89 x7))) (or (or (or (or (or (or (= ?v_90 x1) (= ?v_90 x2)) (= ?v_90 x3)) (= ?v_90 x4)) (= ?v_90 x5)) (= ?v_90 x6)) (= ?v_90 x7))) (or (or (or (or (or (or (= ?v_91 x1) (= ?v_91 x2)) (= ?v_91 x3)) (= ?v_91 x4)) (= ?v_91 x5)) (= ?v_91 x6)) (= ?v_91 x7))) (or (or (or (or (or (or (= ?v_92 x1) (= ?v_92 x2)) (= ?v_92 x3)) (= ?v_92 x4)) (= ?v_92 x5)) (= ?v_92 x6)) (= ?v_92 x7))) (or (or (or (or (or (or (= ?v_93 x1) (= ?v_93 x2)) (= ?v_93 x3)) (= ?v_93 x4)) (= ?v_93 x5)) (= ?v_93 x6)) (= ?v_93 x7))) (or (or (or (or (or (or (= ?v_94 x1) (= ?v_94 x2)) (= ?v_94 x3)) (= ?v_94 x4)) (= ?v_94 x5)) (= ?v_94 x6)) (= ?v_94 x7))) (or (or (or (or (or (or (= ?v_95 x1) (= ?v_95 x2)) (= ?v_95 x3)) (= ?v_95 x4)) (= ?v_95 x5)) (= ?v_95 x6)) (= ?v_95 x7))) (or (or (or (or (or (or (= ?v_96 x1) (= ?v_96 x2)) (= ?v_96 x3)) (= ?v_96 x4)) (= ?v_96 x5)) (= ?v_96 x6)) (= ?v_96 x7))) (or (or (or (or (or (or (= ?v_97 x1) (= ?v_97 x2)) (= ?v_97 x3)) (= ?v_97 x4)) (= ?v_97 x5)) (= ?v_97 x6)) (= ?v_97 x7))) (or (or (or (or (or (or (= ?v_98 x1) (= ?v_98 x2)) (= ?v_98 x3)) (= ?v_98 x4)) (= ?v_98 x5)) (= ?v_98 x6)) (= ?v_98 x7))) (or (or (or (or (or (or (= ?v_99 x1) (= ?v_99 x2)) (= ?v_99 x3)) (= ?v_99 x4)) (= ?v_99 x5)) (= ?v_99 x6)) (= ?v_99 x7))) (or (or (or (or (or (or (= ?v_100 x1) (= ?v_100 x2)) (= ?v_100 x3)) (= ?v_100 x4)) (= ?v_100 x5)) (= ?v_100 x6)) (= ?v_100 x7))) (or (or (or (or (or (or (= ?v_101 x1) (= ?v_101 x2)) (= ?v_101 x3)) (= ?v_101 x4)) (= ?v_101 x5)) (= ?v_101 x6)) (= ?v_101 x7))) (or (or (or (or (or (or (= ?v_102 x1) (= ?v_102 x2)) (= ?v_102 x3)) (= ?v_102 x4)) (= ?v_102 x5)) (= ?v_102 x6)) (= ?v_102 x7))) (or (or (or (or (or (or (= ?v_103 x1) (= ?v_103 x2)) (= ?v_103 x3)) (= ?v_103 x4)) (= ?v_103 x5)) (= ?v_103 x6)) (= ?v_103 x7))) (or (or (or (or (or (or (= ?v_104 x1) (= ?v_104 x2)) (= ?v_104 x3)) (= ?v_104 x4)) (= ?v_104 x5)) (= ?v_104 x6)) (= ?v_104 x7))) (or (or (or (or (or (or (= ?v_105 x1) (= ?v_105 x2)) (= ?v_105 x3)) (= ?v_105 x4)) (= ?v_105 x5)) (= ?v_105 x6)) (= ?v_105 x7))) (or (or (or (or (or (or (= ?v_106 x1) (= ?v_106 x2)) (= ?v_106 x3)) (= ?v_106 x4)) (= ?v_106 x5)) (= ?v_106 x6)) (= ?v_106 x7))) (or (or (or (or (or (or (= ?v_107 x1) (= ?v_107 x2)) (= ?v_107 x3)) (= ?v_107 x4)) (= ?v_107 x5)) (= ?v_107 x6)) (= ?v_107 x7))) (or (or (or (or (or (or (= ?v_108 x1) (= ?v_108 x2)) (= ?v_108 x3)) (= ?v_108 x4)) (= ?v_108 x5)) (= ?v_108 x6)) (= ?v_108 x7))) (or (or (or (or (or (or (= ?v_109 x1) (= ?v_109 x2)) (= ?v_109 x3)) (= ?v_109 x4)) (= ?v_109 x5)) (= ?v_109 x6)) (= ?v_109 x7))) (or (or (or (or (or (or (= ?v_110 x1) (= ?v_110 x2)) (= ?v_110 x3)) (= ?v_110 x4)) (= ?v_110 x5)) (= ?v_110 x6)) (= ?v_110 x7))) (or (or (or (or (or (or (= ?v_111 x1) (= ?v_111 x2)) (= ?v_111 x3)) (= ?v_111 x4)) (= ?v_111 x5)) (= ?v_111 x6)) (= ?v_111 x7))) (or (or (or (or (or (or (= ?v_112 x1) (= ?v_112 x2)) (= ?v_112 x3)) (= ?v_112 x4)) (= ?v_112 x5)) (= ?v_112 x6)) (= ?v_112 x7))) (or (or (or (or (or (or (= ?v_113 x1) (= ?v_113 x2)) (= ?v_113 x3)) (= ?v_113 x4)) (= ?v_113 x5)) (= ?v_113 x6)) (= ?v_113 x7))) (or (or (or (or (or (or (= ?v_114 x1) (= ?v_114 x2)) (= ?v_114 x3)) (= ?v_114 x4)) (= ?v_114 x5)) (= ?v_114 x6)) (= ?v_114 x7))) (or (or (or (or (or (or (= ?v_115 x1) (= ?v_115 x2)) (= ?v_115 x3)) (= ?v_115 x4)) (= ?v_115 x5)) (= ?v_115 x6)) (= ?v_115 x7))) (or (or (or (or (or (or (= ?v_116 x1) (= ?v_116 x2)) (= ?v_116 x3)) (= ?v_116 x4)) (= ?v_116 x5)) (= ?v_116 x6)) (= ?v_116 x7))) (or (or (or (or (or (or (= ?v_117 x1) (= ?v_117 x2)) (= ?v_117 x3)) (= ?v_117 x4)) (= ?v_117 x5)) (= ?v_117 x6)) (= ?v_117 x7))) (or (or (or (or (or (or (= ?v_118 x1) (= ?v_118 x2)) (= ?v_118 x3)) (= ?v_118 x4)) (= ?v_118 x5)) (= ?v_118 x6)) (= ?v_118 x7))) (distinct x1 x2)) (distinct x1 x3)) (distinct x1 x4)) (distinct x1 x5)) (distinct x1 x6)) (distinct x1 x7)) (distinct x2 x3)) (distinct x2 x4)) (distinct x2 x5)) (distinct x2 x6)) (distinct x2 x7)) (distinct x3 x4)) (distinct x3 x5)) (distinct x3 x6)) (distinct x3 x7)) (distinct x4 x5)) (distinct x4 x6)) (distinct x4 x7)) (distinct x5 x6)) (distinct x5 x7)) (distinct x6 x7)) (<= 0 x1)) (< x1 8)) (<= 0 x2)) (< x2 8)) (<= 0 x3)) (< x3 8)) (<= 0 x4)) (< x4 8)) (<= 0 x5)) (< x5 8)) (<= 0 x6)) (< x6 8)) (<= 0 x7)) (< x7 8)) (= (hash_1 (hash_1 (hash_17 (ite (< ?v_119 8) ?v_119 x1)))) (hash_1 (hash_1 (hash_17 (ite (< ?v_120 8) ?v_120 x1)))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/hash_sat_09_09.smt2 b/test/regress/regress1/hash_sat_09_09.smt2 new file mode 100644 index 000000000..6dc26542e --- /dev/null +++ b/test/regress/regress1/hash_sat_09_09.smt2 @@ -0,0 +1,26 @@ +(set-logic QF_UFLIA) +(set-info :source | MathSat group |) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun hash_1 (Int) Int) +(declare-fun hash_2 (Int) Int) +(declare-fun hash_3 (Int) Int) +(declare-fun hash_4 (Int) Int) +(declare-fun hash_5 (Int) Int) +(declare-fun hash_6 (Int) Int) +(declare-fun hash_7 (Int) Int) +(declare-fun hash_8 (Int) Int) +(declare-fun hash_9 (Int) Int) +(declare-fun x1 () Int) +(declare-fun x2 () Int) +(declare-fun x3 () Int) +(declare-fun x4 () Int) +(declare-fun x5 () Int) +(declare-fun x6 () Int) +(declare-fun x7 () Int) +(declare-fun x8 () Int) +(declare-fun x9 () Int) +(assert (let ((?v_0 (hash_1 x1)) (?v_1 (hash_1 x2)) (?v_2 (hash_1 x3)) (?v_3 (hash_1 x4)) (?v_4 (hash_1 x5)) (?v_5 (hash_1 x6)) (?v_6 (hash_1 x7)) (?v_7 (hash_1 x8)) (?v_8 (hash_1 x9)) (?v_9 (hash_2 x1)) (?v_10 (hash_2 x2)) (?v_11 (hash_2 x3)) (?v_12 (hash_2 x4)) (?v_13 (hash_2 x5)) (?v_14 (hash_2 x6)) (?v_15 (hash_2 x7)) (?v_16 (hash_2 x8)) (?v_17 (hash_2 x9)) (?v_18 (hash_3 x1)) (?v_19 (hash_3 x2)) (?v_20 (hash_3 x3)) (?v_21 (hash_3 x4)) (?v_22 (hash_3 x5)) (?v_23 (hash_3 x6)) (?v_24 (hash_3 x7)) (?v_25 (hash_3 x8)) (?v_26 (hash_3 x9)) (?v_27 (hash_4 x1)) (?v_28 (hash_4 x2)) (?v_29 (hash_4 x3)) (?v_30 (hash_4 x4)) (?v_31 (hash_4 x5)) (?v_32 (hash_4 x6)) (?v_33 (hash_4 x7)) (?v_34 (hash_4 x8)) (?v_35 (hash_4 x9)) (?v_36 (hash_5 x1)) (?v_37 (hash_5 x2)) (?v_38 (hash_5 x3)) (?v_39 (hash_5 x4)) (?v_40 (hash_5 x5)) (?v_41 (hash_5 x6)) (?v_42 (hash_5 x7)) (?v_43 (hash_5 x8)) (?v_44 (hash_5 x9)) (?v_45 (hash_6 x1)) (?v_46 (hash_6 x2)) (?v_47 (hash_6 x3)) (?v_48 (hash_6 x4)) (?v_49 (hash_6 x5)) (?v_50 (hash_6 x6)) (?v_51 (hash_6 x7)) (?v_52 (hash_6 x8)) (?v_53 (hash_6 x9)) (?v_54 (hash_7 x1)) (?v_55 (hash_7 x2)) (?v_56 (hash_7 x3)) (?v_57 (hash_7 x4)) (?v_58 (hash_7 x5)) (?v_59 (hash_7 x6)) (?v_60 (hash_7 x7)) (?v_61 (hash_7 x8)) (?v_62 (hash_7 x9)) (?v_63 (hash_8 x1)) (?v_64 (hash_8 x2)) (?v_65 (hash_8 x3)) (?v_66 (hash_8 x4)) (?v_67 (hash_8 x5)) (?v_68 (hash_8 x6)) (?v_69 (hash_8 x7)) (?v_70 (hash_8 x8)) (?v_71 (hash_8 x9)) (?v_72 (hash_9 x1)) (?v_73 (hash_9 x2)) (?v_74 (hash_9 x3)) (?v_75 (hash_9 x4)) (?v_76 (hash_9 x5)) (?v_77 (hash_9 x6)) (?v_78 (hash_9 x7)) (?v_79 (hash_9 x8)) (?v_80 (hash_9 x9)) (?v_81 (+ x1 x9)) (?v_82 (+ x1 x2))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (distinct ?v_0 ?v_1) (distinct ?v_0 ?v_2)) (distinct ?v_0 ?v_3)) (distinct ?v_0 ?v_4)) (distinct ?v_0 ?v_5)) (distinct ?v_0 ?v_6)) (distinct ?v_0 ?v_7)) (distinct ?v_0 ?v_8)) (distinct ?v_1 ?v_2)) (distinct ?v_1 ?v_3)) (distinct ?v_1 ?v_4)) (distinct ?v_1 ?v_5)) (distinct ?v_1 ?v_6)) (distinct ?v_1 ?v_7)) (distinct ?v_1 ?v_8)) (distinct ?v_2 ?v_3)) (distinct ?v_2 ?v_4)) (distinct ?v_2 ?v_5)) (distinct ?v_2 ?v_6)) (distinct ?v_2 ?v_7)) (distinct ?v_2 ?v_8)) (distinct ?v_3 ?v_4)) (distinct ?v_3 ?v_5)) (distinct ?v_3 ?v_6)) (distinct ?v_3 ?v_7)) (distinct ?v_3 ?v_8)) (distinct ?v_4 ?v_5)) (distinct ?v_4 ?v_6)) (distinct ?v_4 ?v_7)) (distinct ?v_4 ?v_8)) (distinct ?v_5 ?v_6)) (distinct ?v_5 ?v_7)) (distinct ?v_5 ?v_8)) (distinct ?v_6 ?v_7)) (distinct ?v_6 ?v_8)) (distinct ?v_7 ?v_8)) (distinct ?v_9 ?v_10)) (distinct ?v_9 ?v_11)) (distinct ?v_9 ?v_12)) (distinct ?v_9 ?v_13)) (distinct ?v_9 ?v_14)) (distinct ?v_9 ?v_15)) (distinct ?v_9 ?v_16)) (distinct ?v_9 ?v_17)) (distinct ?v_10 ?v_11)) (distinct ?v_10 ?v_12)) (distinct ?v_10 ?v_13)) (distinct ?v_10 ?v_14)) (distinct ?v_10 ?v_15)) (distinct ?v_10 ?v_16)) (distinct ?v_10 ?v_17)) (distinct ?v_11 ?v_12)) (distinct ?v_11 ?v_13)) (distinct ?v_11 ?v_14)) (distinct ?v_11 ?v_15)) (distinct ?v_11 ?v_16)) (distinct ?v_11 ?v_17)) (distinct ?v_12 ?v_13)) (distinct ?v_12 ?v_14)) (distinct ?v_12 ?v_15)) (distinct ?v_12 ?v_16)) (distinct ?v_12 ?v_17)) (distinct ?v_13 ?v_14)) (distinct ?v_13 ?v_15)) (distinct ?v_13 ?v_16)) (distinct ?v_13 ?v_17)) (distinct ?v_14 ?v_15)) (distinct ?v_14 ?v_16)) (distinct ?v_14 ?v_17)) (distinct ?v_15 ?v_16)) (distinct ?v_15 ?v_17)) (distinct ?v_16 ?v_17)) (distinct ?v_18 ?v_19)) (distinct ?v_18 ?v_20)) (distinct ?v_18 ?v_21)) (distinct ?v_18 ?v_22)) (distinct ?v_18 ?v_23)) (distinct ?v_18 ?v_24)) (distinct ?v_18 ?v_25)) (distinct ?v_18 ?v_26)) (distinct ?v_19 ?v_20)) (distinct ?v_19 ?v_21)) (distinct ?v_19 ?v_22)) (distinct ?v_19 ?v_23)) (distinct ?v_19 ?v_24)) (distinct ?v_19 ?v_25)) (distinct ?v_19 ?v_26)) (distinct ?v_20 ?v_21)) (distinct ?v_20 ?v_22)) (distinct ?v_20 ?v_23)) (distinct ?v_20 ?v_24)) (distinct ?v_20 ?v_25)) (distinct ?v_20 ?v_26)) (distinct ?v_21 ?v_22)) (distinct ?v_21 ?v_23)) (distinct ?v_21 ?v_24)) (distinct ?v_21 ?v_25)) (distinct ?v_21 ?v_26)) (distinct ?v_22 ?v_23)) (distinct ?v_22 ?v_24)) (distinct ?v_22 ?v_25)) (distinct ?v_22 ?v_26)) (distinct ?v_23 ?v_24)) (distinct ?v_23 ?v_25)) (distinct ?v_23 ?v_26)) (distinct ?v_24 ?v_25)) (distinct ?v_24 ?v_26)) (distinct ?v_25 ?v_26)) (distinct ?v_27 ?v_28)) (distinct ?v_27 ?v_29)) (distinct ?v_27 ?v_30)) (distinct ?v_27 ?v_31)) (distinct ?v_27 ?v_32)) (distinct ?v_27 ?v_33)) (distinct ?v_27 ?v_34)) (distinct ?v_27 ?v_35)) (distinct ?v_28 ?v_29)) (distinct ?v_28 ?v_30)) (distinct ?v_28 ?v_31)) (distinct ?v_28 ?v_32)) (distinct ?v_28 ?v_33)) (distinct ?v_28 ?v_34)) (distinct ?v_28 ?v_35)) (distinct ?v_29 ?v_30)) (distinct ?v_29 ?v_31)) (distinct ?v_29 ?v_32)) (distinct ?v_29 ?v_33)) (distinct ?v_29 ?v_34)) (distinct ?v_29 ?v_35)) (distinct ?v_30 ?v_31)) (distinct ?v_30 ?v_32)) (distinct ?v_30 ?v_33)) (distinct ?v_30 ?v_34)) (distinct ?v_30 ?v_35)) (distinct ?v_31 ?v_32)) (distinct ?v_31 ?v_33)) (distinct ?v_31 ?v_34)) (distinct ?v_31 ?v_35)) (distinct ?v_32 ?v_33)) (distinct ?v_32 ?v_34)) (distinct ?v_32 ?v_35)) (distinct ?v_33 ?v_34)) (distinct ?v_33 ?v_35)) (distinct ?v_34 ?v_35)) (distinct ?v_36 ?v_37)) (distinct ?v_36 ?v_38)) (distinct ?v_36 ?v_39)) (distinct ?v_36 ?v_40)) (distinct ?v_36 ?v_41)) (distinct ?v_36 ?v_42)) (distinct ?v_36 ?v_43)) (distinct ?v_36 ?v_44)) (distinct ?v_37 ?v_38)) (distinct ?v_37 ?v_39)) (distinct ?v_37 ?v_40)) (distinct ?v_37 ?v_41)) (distinct ?v_37 ?v_42)) (distinct ?v_37 ?v_43)) (distinct ?v_37 ?v_44)) (distinct ?v_38 ?v_39)) (distinct ?v_38 ?v_40)) (distinct ?v_38 ?v_41)) (distinct ?v_38 ?v_42)) (distinct ?v_38 ?v_43)) (distinct ?v_38 ?v_44)) (distinct ?v_39 ?v_40)) (distinct ?v_39 ?v_41)) (distinct ?v_39 ?v_42)) (distinct ?v_39 ?v_43)) (distinct ?v_39 ?v_44)) (distinct ?v_40 ?v_41)) (distinct ?v_40 ?v_42)) (distinct ?v_40 ?v_43)) (distinct ?v_40 ?v_44)) (distinct ?v_41 ?v_42)) (distinct ?v_41 ?v_43)) (distinct ?v_41 ?v_44)) (distinct ?v_42 ?v_43)) (distinct ?v_42 ?v_44)) (distinct ?v_43 ?v_44)) (distinct ?v_45 ?v_46)) (distinct ?v_45 ?v_47)) (distinct ?v_45 ?v_48)) (distinct ?v_45 ?v_49)) (distinct ?v_45 ?v_50)) (distinct ?v_45 ?v_51)) (distinct ?v_45 ?v_52)) (distinct ?v_45 ?v_53)) (distinct ?v_46 ?v_47)) (distinct ?v_46 ?v_48)) (distinct ?v_46 ?v_49)) (distinct ?v_46 ?v_50)) (distinct ?v_46 ?v_51)) (distinct ?v_46 ?v_52)) (distinct ?v_46 ?v_53)) (distinct ?v_47 ?v_48)) (distinct ?v_47 ?v_49)) (distinct ?v_47 ?v_50)) (distinct ?v_47 ?v_51)) (distinct ?v_47 ?v_52)) (distinct ?v_47 ?v_53)) (distinct ?v_48 ?v_49)) (distinct ?v_48 ?v_50)) (distinct ?v_48 ?v_51)) (distinct ?v_48 ?v_52)) (distinct ?v_48 ?v_53)) (distinct ?v_49 ?v_50)) (distinct ?v_49 ?v_51)) (distinct ?v_49 ?v_52)) (distinct ?v_49 ?v_53)) (distinct ?v_50 ?v_51)) (distinct ?v_50 ?v_52)) (distinct ?v_50 ?v_53)) (distinct ?v_51 ?v_52)) (distinct ?v_51 ?v_53)) (distinct ?v_52 ?v_53)) (distinct ?v_54 ?v_55)) (distinct ?v_54 ?v_56)) (distinct ?v_54 ?v_57)) (distinct ?v_54 ?v_58)) (distinct ?v_54 ?v_59)) (distinct ?v_54 ?v_60)) (distinct ?v_54 ?v_61)) (distinct ?v_54 ?v_62)) (distinct ?v_55 ?v_56)) (distinct ?v_55 ?v_57)) (distinct ?v_55 ?v_58)) (distinct ?v_55 ?v_59)) (distinct ?v_55 ?v_60)) (distinct ?v_55 ?v_61)) (distinct ?v_55 ?v_62)) (distinct ?v_56 ?v_57)) (distinct ?v_56 ?v_58)) (distinct ?v_56 ?v_59)) (distinct ?v_56 ?v_60)) (distinct ?v_56 ?v_61)) (distinct ?v_56 ?v_62)) (distinct ?v_57 ?v_58)) (distinct ?v_57 ?v_59)) (distinct ?v_57 ?v_60)) (distinct ?v_57 ?v_61)) (distinct ?v_57 ?v_62)) (distinct ?v_58 ?v_59)) (distinct ?v_58 ?v_60)) (distinct ?v_58 ?v_61)) (distinct ?v_58 ?v_62)) (distinct ?v_59 ?v_60)) (distinct ?v_59 ?v_61)) (distinct ?v_59 ?v_62)) (distinct ?v_60 ?v_61)) (distinct ?v_60 ?v_62)) (distinct ?v_61 ?v_62)) (distinct ?v_63 ?v_64)) (distinct ?v_63 ?v_65)) (distinct ?v_63 ?v_66)) (distinct ?v_63 ?v_67)) (distinct ?v_63 ?v_68)) (distinct ?v_63 ?v_69)) (distinct ?v_63 ?v_70)) (distinct ?v_63 ?v_71)) (distinct ?v_64 ?v_65)) (distinct ?v_64 ?v_66)) (distinct ?v_64 ?v_67)) (distinct ?v_64 ?v_68)) (distinct ?v_64 ?v_69)) (distinct ?v_64 ?v_70)) (distinct ?v_64 ?v_71)) (distinct ?v_65 ?v_66)) (distinct ?v_65 ?v_67)) (distinct ?v_65 ?v_68)) (distinct ?v_65 ?v_69)) (distinct ?v_65 ?v_70)) (distinct ?v_65 ?v_71)) (distinct ?v_66 ?v_67)) (distinct ?v_66 ?v_68)) (distinct ?v_66 ?v_69)) (distinct ?v_66 ?v_70)) (distinct ?v_66 ?v_71)) (distinct ?v_67 ?v_68)) (distinct ?v_67 ?v_69)) (distinct ?v_67 ?v_70)) (distinct ?v_67 ?v_71)) (distinct ?v_68 ?v_69)) (distinct ?v_68 ?v_70)) (distinct ?v_68 ?v_71)) (distinct ?v_69 ?v_70)) (distinct ?v_69 ?v_71)) (distinct ?v_70 ?v_71)) (distinct ?v_72 ?v_73)) (distinct ?v_72 ?v_74)) (distinct ?v_72 ?v_75)) (distinct ?v_72 ?v_76)) (distinct ?v_72 ?v_77)) (distinct ?v_72 ?v_78)) (distinct ?v_72 ?v_79)) (distinct ?v_72 ?v_80)) (distinct ?v_73 ?v_74)) (distinct ?v_73 ?v_75)) (distinct ?v_73 ?v_76)) (distinct ?v_73 ?v_77)) (distinct ?v_73 ?v_78)) (distinct ?v_73 ?v_79)) (distinct ?v_73 ?v_80)) (distinct ?v_74 ?v_75)) (distinct ?v_74 ?v_76)) (distinct ?v_74 ?v_77)) (distinct ?v_74 ?v_78)) (distinct ?v_74 ?v_79)) (distinct ?v_74 ?v_80)) (distinct ?v_75 ?v_76)) (distinct ?v_75 ?v_77)) (distinct ?v_75 ?v_78)) (distinct ?v_75 ?v_79)) (distinct ?v_75 ?v_80)) (distinct ?v_76 ?v_77)) (distinct ?v_76 ?v_78)) (distinct ?v_76 ?v_79)) (distinct ?v_76 ?v_80)) (distinct ?v_77 ?v_78)) (distinct ?v_77 ?v_79)) (distinct ?v_77 ?v_80)) (distinct ?v_78 ?v_79)) (distinct ?v_78 ?v_80)) (distinct ?v_79 ?v_80)) (or (or (or (or (or (or (or (or (= ?v_0 x1) (= ?v_0 x2)) (= ?v_0 x3)) (= ?v_0 x4)) (= ?v_0 x5)) (= ?v_0 x6)) (= ?v_0 x7)) (= ?v_0 x8)) (= ?v_0 x9))) (or (or (or (or (or (or (or (or (= ?v_1 x1) (= ?v_1 x2)) (= ?v_1 x3)) (= ?v_1 x4)) (= ?v_1 x5)) (= ?v_1 x6)) (= ?v_1 x7)) (= ?v_1 x8)) (= ?v_1 x9))) (or (or (or (or (or (or (or (or (= ?v_2 x1) (= ?v_2 x2)) (= ?v_2 x3)) (= ?v_2 x4)) (= ?v_2 x5)) (= ?v_2 x6)) (= ?v_2 x7)) (= ?v_2 x8)) (= ?v_2 x9))) (or (or (or (or (or (or (or (or (= ?v_3 x1) (= ?v_3 x2)) (= ?v_3 x3)) (= ?v_3 x4)) (= ?v_3 x5)) (= ?v_3 x6)) (= ?v_3 x7)) (= ?v_3 x8)) (= ?v_3 x9))) (or (or (or (or (or (or (or (or (= ?v_4 x1) (= ?v_4 x2)) (= ?v_4 x3)) (= ?v_4 x4)) (= ?v_4 x5)) (= ?v_4 x6)) (= ?v_4 x7)) (= ?v_4 x8)) (= ?v_4 x9))) (or (or (or (or (or (or (or (or (= ?v_5 x1) (= ?v_5 x2)) (= ?v_5 x3)) (= ?v_5 x4)) (= ?v_5 x5)) (= ?v_5 x6)) (= ?v_5 x7)) (= ?v_5 x8)) (= ?v_5 x9))) (or (or (or (or (or (or (or (or (= ?v_6 x1) (= ?v_6 x2)) (= ?v_6 x3)) (= ?v_6 x4)) (= ?v_6 x5)) (= ?v_6 x6)) (= ?v_6 x7)) (= ?v_6 x8)) (= ?v_6 x9))) (or (or (or (or (or (or (or (or (= ?v_7 x1) (= ?v_7 x2)) (= ?v_7 x3)) (= ?v_7 x4)) (= ?v_7 x5)) (= ?v_7 x6)) (= ?v_7 x7)) (= ?v_7 x8)) (= ?v_7 x9))) (or (or (or (or (or (or (or (or (= ?v_8 x1) (= ?v_8 x2)) (= ?v_8 x3)) (= ?v_8 x4)) (= ?v_8 x5)) (= ?v_8 x6)) (= ?v_8 x7)) (= ?v_8 x8)) (= ?v_8 x9))) (or (or (or (or (or (or (or (or (= ?v_9 x1) (= ?v_9 x2)) (= ?v_9 x3)) (= ?v_9 x4)) (= ?v_9 x5)) (= ?v_9 x6)) (= ?v_9 x7)) (= ?v_9 x8)) (= ?v_9 x9))) (or (or (or (or (or (or (or (or (= ?v_10 x1) (= ?v_10 x2)) (= ?v_10 x3)) (= ?v_10 x4)) (= ?v_10 x5)) (= ?v_10 x6)) (= ?v_10 x7)) (= ?v_10 x8)) (= ?v_10 x9))) (or (or (or (or (or (or (or (or (= ?v_11 x1) (= ?v_11 x2)) (= ?v_11 x3)) (= ?v_11 x4)) (= ?v_11 x5)) (= ?v_11 x6)) (= ?v_11 x7)) (= ?v_11 x8)) (= ?v_11 x9))) (or (or (or (or (or (or (or (or (= ?v_12 x1) (= ?v_12 x2)) (= ?v_12 x3)) (= ?v_12 x4)) (= ?v_12 x5)) (= ?v_12 x6)) (= ?v_12 x7)) (= ?v_12 x8)) (= ?v_12 x9))) (or (or (or (or (or (or (or (or (= ?v_13 x1) (= ?v_13 x2)) (= ?v_13 x3)) (= ?v_13 x4)) (= ?v_13 x5)) (= ?v_13 x6)) (= ?v_13 x7)) (= ?v_13 x8)) (= ?v_13 x9))) (or (or (or (or (or (or (or (or (= ?v_14 x1) (= ?v_14 x2)) (= ?v_14 x3)) (= ?v_14 x4)) (= ?v_14 x5)) (= ?v_14 x6)) (= ?v_14 x7)) (= ?v_14 x8)) (= ?v_14 x9))) (or (or (or (or (or (or (or (or (= ?v_15 x1) (= ?v_15 x2)) (= ?v_15 x3)) (= ?v_15 x4)) (= ?v_15 x5)) (= ?v_15 x6)) (= ?v_15 x7)) (= ?v_15 x8)) (= ?v_15 x9))) (or (or (or (or (or (or (or (or (= ?v_16 x1) (= ?v_16 x2)) (= ?v_16 x3)) (= ?v_16 x4)) (= ?v_16 x5)) (= ?v_16 x6)) (= ?v_16 x7)) (= ?v_16 x8)) (= ?v_16 x9))) (or (or (or (or (or (or (or (or (= ?v_17 x1) (= ?v_17 x2)) (= ?v_17 x3)) (= ?v_17 x4)) (= ?v_17 x5)) (= ?v_17 x6)) (= ?v_17 x7)) (= ?v_17 x8)) (= ?v_17 x9))) (or (or (or (or (or (or (or (or (= ?v_18 x1) (= ?v_18 x2)) (= ?v_18 x3)) (= ?v_18 x4)) (= ?v_18 x5)) (= ?v_18 x6)) (= ?v_18 x7)) (= ?v_18 x8)) (= ?v_18 x9))) (or (or (or (or (or (or (or (or (= ?v_19 x1) (= ?v_19 x2)) (= ?v_19 x3)) (= ?v_19 x4)) (= ?v_19 x5)) (= ?v_19 x6)) (= ?v_19 x7)) (= ?v_19 x8)) (= ?v_19 x9))) (or (or (or (or (or (or (or (or (= ?v_20 x1) (= ?v_20 x2)) (= ?v_20 x3)) (= ?v_20 x4)) (= ?v_20 x5)) (= ?v_20 x6)) (= ?v_20 x7)) (= ?v_20 x8)) (= ?v_20 x9))) (or (or (or (or (or (or (or (or (= ?v_21 x1) (= ?v_21 x2)) (= ?v_21 x3)) (= ?v_21 x4)) (= ?v_21 x5)) (= ?v_21 x6)) (= ?v_21 x7)) (= ?v_21 x8)) (= ?v_21 x9))) (or (or (or (or (or (or (or (or (= ?v_22 x1) (= ?v_22 x2)) (= ?v_22 x3)) (= ?v_22 x4)) (= ?v_22 x5)) (= ?v_22 x6)) (= ?v_22 x7)) (= ?v_22 x8)) (= ?v_22 x9))) (or (or (or (or (or (or (or (or (= ?v_23 x1) (= ?v_23 x2)) (= ?v_23 x3)) (= ?v_23 x4)) (= ?v_23 x5)) (= ?v_23 x6)) (= ?v_23 x7)) (= ?v_23 x8)) (= ?v_23 x9))) (or (or (or (or (or (or (or (or (= ?v_24 x1) (= ?v_24 x2)) (= ?v_24 x3)) (= ?v_24 x4)) (= ?v_24 x5)) (= ?v_24 x6)) (= ?v_24 x7)) (= ?v_24 x8)) (= ?v_24 x9))) (or (or (or (or (or (or (or (or (= ?v_25 x1) (= ?v_25 x2)) (= ?v_25 x3)) (= ?v_25 x4)) (= ?v_25 x5)) (= ?v_25 x6)) (= ?v_25 x7)) (= ?v_25 x8)) (= ?v_25 x9))) (or (or (or (or (or (or (or (or (= ?v_26 x1) (= ?v_26 x2)) (= ?v_26 x3)) (= ?v_26 x4)) (= ?v_26 x5)) (= ?v_26 x6)) (= ?v_26 x7)) (= ?v_26 x8)) (= ?v_26 x9))) (or (or (or (or (or (or (or (or (= ?v_27 x1) (= ?v_27 x2)) (= ?v_27 x3)) (= ?v_27 x4)) (= ?v_27 x5)) (= ?v_27 x6)) (= ?v_27 x7)) (= ?v_27 x8)) (= ?v_27 x9))) (or (or (or (or (or (or (or (or (= ?v_28 x1) (= ?v_28 x2)) (= ?v_28 x3)) (= ?v_28 x4)) (= ?v_28 x5)) (= ?v_28 x6)) (= ?v_28 x7)) (= ?v_28 x8)) (= ?v_28 x9))) (or (or (or (or (or (or (or (or (= ?v_29 x1) (= ?v_29 x2)) (= ?v_29 x3)) (= ?v_29 x4)) (= ?v_29 x5)) (= ?v_29 x6)) (= ?v_29 x7)) (= ?v_29 x8)) (= ?v_29 x9))) (or (or (or (or (or (or (or (or (= ?v_30 x1) (= ?v_30 x2)) (= ?v_30 x3)) (= ?v_30 x4)) (= ?v_30 x5)) (= ?v_30 x6)) (= ?v_30 x7)) (= ?v_30 x8)) (= ?v_30 x9))) (or (or (or (or (or (or (or (or (= ?v_31 x1) (= ?v_31 x2)) (= ?v_31 x3)) (= ?v_31 x4)) (= ?v_31 x5)) (= ?v_31 x6)) (= ?v_31 x7)) (= ?v_31 x8)) (= ?v_31 x9))) (or (or (or (or (or (or (or (or (= ?v_32 x1) (= ?v_32 x2)) (= ?v_32 x3)) (= ?v_32 x4)) (= ?v_32 x5)) (= ?v_32 x6)) (= ?v_32 x7)) (= ?v_32 x8)) (= ?v_32 x9))) (or (or (or (or (or (or (or (or (= ?v_33 x1) (= ?v_33 x2)) (= ?v_33 x3)) (= ?v_33 x4)) (= ?v_33 x5)) (= ?v_33 x6)) (= ?v_33 x7)) (= ?v_33 x8)) (= ?v_33 x9))) (or (or (or (or (or (or (or (or (= ?v_34 x1) (= ?v_34 x2)) (= ?v_34 x3)) (= ?v_34 x4)) (= ?v_34 x5)) (= ?v_34 x6)) (= ?v_34 x7)) (= ?v_34 x8)) (= ?v_34 x9))) (or (or (or (or (or (or (or (or (= ?v_35 x1) (= ?v_35 x2)) (= ?v_35 x3)) (= ?v_35 x4)) (= ?v_35 x5)) (= ?v_35 x6)) (= ?v_35 x7)) (= ?v_35 x8)) (= ?v_35 x9))) (or (or (or (or (or (or (or (or (= ?v_36 x1) (= ?v_36 x2)) (= ?v_36 x3)) (= ?v_36 x4)) (= ?v_36 x5)) (= ?v_36 x6)) (= ?v_36 x7)) (= ?v_36 x8)) (= ?v_36 x9))) (or (or (or (or (or (or (or (or (= ?v_37 x1) (= ?v_37 x2)) (= ?v_37 x3)) (= ?v_37 x4)) (= ?v_37 x5)) (= ?v_37 x6)) (= ?v_37 x7)) (= ?v_37 x8)) (= ?v_37 x9))) (or (or (or (or (or (or (or (or (= ?v_38 x1) (= ?v_38 x2)) (= ?v_38 x3)) (= ?v_38 x4)) (= ?v_38 x5)) (= ?v_38 x6)) (= ?v_38 x7)) (= ?v_38 x8)) (= ?v_38 x9))) (or (or (or (or (or (or (or (or (= ?v_39 x1) (= ?v_39 x2)) (= ?v_39 x3)) (= ?v_39 x4)) (= ?v_39 x5)) (= ?v_39 x6)) (= ?v_39 x7)) (= ?v_39 x8)) (= ?v_39 x9))) (or (or (or (or (or (or (or (or (= ?v_40 x1) (= ?v_40 x2)) (= ?v_40 x3)) (= ?v_40 x4)) (= ?v_40 x5)) (= ?v_40 x6)) (= ?v_40 x7)) (= ?v_40 x8)) (= ?v_40 x9))) (or (or (or (or (or (or (or (or (= ?v_41 x1) (= ?v_41 x2)) (= ?v_41 x3)) (= ?v_41 x4)) (= ?v_41 x5)) (= ?v_41 x6)) (= ?v_41 x7)) (= ?v_41 x8)) (= ?v_41 x9))) (or (or (or (or (or (or (or (or (= ?v_42 x1) (= ?v_42 x2)) (= ?v_42 x3)) (= ?v_42 x4)) (= ?v_42 x5)) (= ?v_42 x6)) (= ?v_42 x7)) (= ?v_42 x8)) (= ?v_42 x9))) (or (or (or (or (or (or (or (or (= ?v_43 x1) (= ?v_43 x2)) (= ?v_43 x3)) (= ?v_43 x4)) (= ?v_43 x5)) (= ?v_43 x6)) (= ?v_43 x7)) (= ?v_43 x8)) (= ?v_43 x9))) (or (or (or (or (or (or (or (or (= ?v_44 x1) (= ?v_44 x2)) (= ?v_44 x3)) (= ?v_44 x4)) (= ?v_44 x5)) (= ?v_44 x6)) (= ?v_44 x7)) (= ?v_44 x8)) (= ?v_44 x9))) (or (or (or (or (or (or (or (or (= ?v_45 x1) (= ?v_45 x2)) (= ?v_45 x3)) (= ?v_45 x4)) (= ?v_45 x5)) (= ?v_45 x6)) (= ?v_45 x7)) (= ?v_45 x8)) (= ?v_45 x9))) (or (or (or (or (or (or (or (or (= ?v_46 x1) (= ?v_46 x2)) (= ?v_46 x3)) (= ?v_46 x4)) (= ?v_46 x5)) (= ?v_46 x6)) (= ?v_46 x7)) (= ?v_46 x8)) (= ?v_46 x9))) (or (or (or (or (or (or (or (or (= ?v_47 x1) (= ?v_47 x2)) (= ?v_47 x3)) (= ?v_47 x4)) (= ?v_47 x5)) (= ?v_47 x6)) (= ?v_47 x7)) (= ?v_47 x8)) (= ?v_47 x9))) (or (or (or (or (or (or (or (or (= ?v_48 x1) (= ?v_48 x2)) (= ?v_48 x3)) (= ?v_48 x4)) (= ?v_48 x5)) (= ?v_48 x6)) (= ?v_48 x7)) (= ?v_48 x8)) (= ?v_48 x9))) (or (or (or (or (or (or (or (or (= ?v_49 x1) (= ?v_49 x2)) (= ?v_49 x3)) (= ?v_49 x4)) (= ?v_49 x5)) (= ?v_49 x6)) (= ?v_49 x7)) (= ?v_49 x8)) (= ?v_49 x9))) (or (or (or (or (or (or (or (or (= ?v_50 x1) (= ?v_50 x2)) (= ?v_50 x3)) (= ?v_50 x4)) (= ?v_50 x5)) (= ?v_50 x6)) (= ?v_50 x7)) (= ?v_50 x8)) (= ?v_50 x9))) (or (or (or (or (or (or (or (or (= ?v_51 x1) (= ?v_51 x2)) (= ?v_51 x3)) (= ?v_51 x4)) (= ?v_51 x5)) (= ?v_51 x6)) (= ?v_51 x7)) (= ?v_51 x8)) (= ?v_51 x9))) (or (or (or (or (or (or (or (or (= ?v_52 x1) (= ?v_52 x2)) (= ?v_52 x3)) (= ?v_52 x4)) (= ?v_52 x5)) (= ?v_52 x6)) (= ?v_52 x7)) (= ?v_52 x8)) (= ?v_52 x9))) (or (or (or (or (or (or (or (or (= ?v_53 x1) (= ?v_53 x2)) (= ?v_53 x3)) (= ?v_53 x4)) (= ?v_53 x5)) (= ?v_53 x6)) (= ?v_53 x7)) (= ?v_53 x8)) (= ?v_53 x9))) (or (or (or (or (or (or (or (or (= ?v_54 x1) (= ?v_54 x2)) (= ?v_54 x3)) (= ?v_54 x4)) (= ?v_54 x5)) (= ?v_54 x6)) (= ?v_54 x7)) (= ?v_54 x8)) (= ?v_54 x9))) (or (or (or (or (or (or (or (or (= ?v_55 x1) (= ?v_55 x2)) (= ?v_55 x3)) (= ?v_55 x4)) (= ?v_55 x5)) (= ?v_55 x6)) (= ?v_55 x7)) (= ?v_55 x8)) (= ?v_55 x9))) (or (or (or (or (or (or (or (or (= ?v_56 x1) (= ?v_56 x2)) (= ?v_56 x3)) (= ?v_56 x4)) (= ?v_56 x5)) (= ?v_56 x6)) (= ?v_56 x7)) (= ?v_56 x8)) (= ?v_56 x9))) (or (or (or (or (or (or (or (or (= ?v_57 x1) (= ?v_57 x2)) (= ?v_57 x3)) (= ?v_57 x4)) (= ?v_57 x5)) (= ?v_57 x6)) (= ?v_57 x7)) (= ?v_57 x8)) (= ?v_57 x9))) (or (or (or (or (or (or (or (or (= ?v_58 x1) (= ?v_58 x2)) (= ?v_58 x3)) (= ?v_58 x4)) (= ?v_58 x5)) (= ?v_58 x6)) (= ?v_58 x7)) (= ?v_58 x8)) (= ?v_58 x9))) (or (or (or (or (or (or (or (or (= ?v_59 x1) (= ?v_59 x2)) (= ?v_59 x3)) (= ?v_59 x4)) (= ?v_59 x5)) (= ?v_59 x6)) (= ?v_59 x7)) (= ?v_59 x8)) (= ?v_59 x9))) (or (or (or (or (or (or (or (or (= ?v_60 x1) (= ?v_60 x2)) (= ?v_60 x3)) (= ?v_60 x4)) (= ?v_60 x5)) (= ?v_60 x6)) (= ?v_60 x7)) (= ?v_60 x8)) (= ?v_60 x9))) (or (or (or (or (or (or (or (or (= ?v_61 x1) (= ?v_61 x2)) (= ?v_61 x3)) (= ?v_61 x4)) (= ?v_61 x5)) (= ?v_61 x6)) (= ?v_61 x7)) (= ?v_61 x8)) (= ?v_61 x9))) (or (or (or (or (or (or (or (or (= ?v_62 x1) (= ?v_62 x2)) (= ?v_62 x3)) (= ?v_62 x4)) (= ?v_62 x5)) (= ?v_62 x6)) (= ?v_62 x7)) (= ?v_62 x8)) (= ?v_62 x9))) (or (or (or (or (or (or (or (or (= ?v_63 x1) (= ?v_63 x2)) (= ?v_63 x3)) (= ?v_63 x4)) (= ?v_63 x5)) (= ?v_63 x6)) (= ?v_63 x7)) (= ?v_63 x8)) (= ?v_63 x9))) (or (or (or (or (or (or (or (or (= ?v_64 x1) (= ?v_64 x2)) (= ?v_64 x3)) (= ?v_64 x4)) (= ?v_64 x5)) (= ?v_64 x6)) (= ?v_64 x7)) (= ?v_64 x8)) (= ?v_64 x9))) (or (or (or (or (or (or (or (or (= ?v_65 x1) (= ?v_65 x2)) (= ?v_65 x3)) (= ?v_65 x4)) (= ?v_65 x5)) (= ?v_65 x6)) (= ?v_65 x7)) (= ?v_65 x8)) (= ?v_65 x9))) (or (or (or (or (or (or (or (or (= ?v_66 x1) (= ?v_66 x2)) (= ?v_66 x3)) (= ?v_66 x4)) (= ?v_66 x5)) (= ?v_66 x6)) (= ?v_66 x7)) (= ?v_66 x8)) (= ?v_66 x9))) (or (or (or (or (or (or (or (or (= ?v_67 x1) (= ?v_67 x2)) (= ?v_67 x3)) (= ?v_67 x4)) (= ?v_67 x5)) (= ?v_67 x6)) (= ?v_67 x7)) (= ?v_67 x8)) (= ?v_67 x9))) (or (or (or (or (or (or (or (or (= ?v_68 x1) (= ?v_68 x2)) (= ?v_68 x3)) (= ?v_68 x4)) (= ?v_68 x5)) (= ?v_68 x6)) (= ?v_68 x7)) (= ?v_68 x8)) (= ?v_68 x9))) (or (or (or (or (or (or (or (or (= ?v_69 x1) (= ?v_69 x2)) (= ?v_69 x3)) (= ?v_69 x4)) (= ?v_69 x5)) (= ?v_69 x6)) (= ?v_69 x7)) (= ?v_69 x8)) (= ?v_69 x9))) (or (or (or (or (or (or (or (or (= ?v_70 x1) (= ?v_70 x2)) (= ?v_70 x3)) (= ?v_70 x4)) (= ?v_70 x5)) (= ?v_70 x6)) (= ?v_70 x7)) (= ?v_70 x8)) (= ?v_70 x9))) (or (or (or (or (or (or (or (or (= ?v_71 x1) (= ?v_71 x2)) (= ?v_71 x3)) (= ?v_71 x4)) (= ?v_71 x5)) (= ?v_71 x6)) (= ?v_71 x7)) (= ?v_71 x8)) (= ?v_71 x9))) (or (or (or (or (or (or (or (or (= ?v_72 x1) (= ?v_72 x2)) (= ?v_72 x3)) (= ?v_72 x4)) (= ?v_72 x5)) (= ?v_72 x6)) (= ?v_72 x7)) (= ?v_72 x8)) (= ?v_72 x9))) (or (or (or (or (or (or (or (or (= ?v_73 x1) (= ?v_73 x2)) (= ?v_73 x3)) (= ?v_73 x4)) (= ?v_73 x5)) (= ?v_73 x6)) (= ?v_73 x7)) (= ?v_73 x8)) (= ?v_73 x9))) (or (or (or (or (or (or (or (or (= ?v_74 x1) (= ?v_74 x2)) (= ?v_74 x3)) (= ?v_74 x4)) (= ?v_74 x5)) (= ?v_74 x6)) (= ?v_74 x7)) (= ?v_74 x8)) (= ?v_74 x9))) (or (or (or (or (or (or (or (or (= ?v_75 x1) (= ?v_75 x2)) (= ?v_75 x3)) (= ?v_75 x4)) (= ?v_75 x5)) (= ?v_75 x6)) (= ?v_75 x7)) (= ?v_75 x8)) (= ?v_75 x9))) (or (or (or (or (or (or (or (or (= ?v_76 x1) (= ?v_76 x2)) (= ?v_76 x3)) (= ?v_76 x4)) (= ?v_76 x5)) (= ?v_76 x6)) (= ?v_76 x7)) (= ?v_76 x8)) (= ?v_76 x9))) (or (or (or (or (or (or (or (or (= ?v_77 x1) (= ?v_77 x2)) (= ?v_77 x3)) (= ?v_77 x4)) (= ?v_77 x5)) (= ?v_77 x6)) (= ?v_77 x7)) (= ?v_77 x8)) (= ?v_77 x9))) (or (or (or (or (or (or (or (or (= ?v_78 x1) (= ?v_78 x2)) (= ?v_78 x3)) (= ?v_78 x4)) (= ?v_78 x5)) (= ?v_78 x6)) (= ?v_78 x7)) (= ?v_78 x8)) (= ?v_78 x9))) (or (or (or (or (or (or (or (or (= ?v_79 x1) (= ?v_79 x2)) (= ?v_79 x3)) (= ?v_79 x4)) (= ?v_79 x5)) (= ?v_79 x6)) (= ?v_79 x7)) (= ?v_79 x8)) (= ?v_79 x9))) (or (or (or (or (or (or (or (or (= ?v_80 x1) (= ?v_80 x2)) (= ?v_80 x3)) (= ?v_80 x4)) (= ?v_80 x5)) (= ?v_80 x6)) (= ?v_80 x7)) (= ?v_80 x8)) (= ?v_80 x9))) (distinct x1 x2)) (distinct x1 x3)) (distinct x1 x4)) (distinct x1 x5)) (distinct x1 x6)) (distinct x1 x7)) (distinct x1 x8)) (distinct x1 x9)) (distinct x2 x3)) (distinct x2 x4)) (distinct x2 x5)) (distinct x2 x6)) (distinct x2 x7)) (distinct x2 x8)) (distinct x2 x9)) (distinct x3 x4)) (distinct x3 x5)) (distinct x3 x6)) (distinct x3 x7)) (distinct x3 x8)) (distinct x3 x9)) (distinct x4 x5)) (distinct x4 x6)) (distinct x4 x7)) (distinct x4 x8)) (distinct x4 x9)) (distinct x5 x6)) (distinct x5 x7)) (distinct x5 x8)) (distinct x5 x9)) (distinct x6 x7)) (distinct x6 x8)) (distinct x6 x9)) (distinct x7 x8)) (distinct x7 x9)) (distinct x8 x9)) (<= 0 x1)) (< x1 10)) (<= 0 x2)) (< x2 10)) (<= 0 x3)) (< x3 10)) (<= 0 x4)) (< x4 10)) (<= 0 x5)) (< x5 10)) (<= 0 x6)) (< x6 10)) (<= 0 x7)) (< x7 10)) (<= 0 x8)) (< x8 10)) (<= 0 x9)) (< x9 10)) (= (hash_1 (hash_1 (hash_9 (ite (< ?v_81 10) ?v_81 x1)))) (hash_1 (hash_1 (hash_9 (ite (< ?v_82 10) ?v_82 x1)))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/hash_sat_10_09.smt2 b/test/regress/regress1/hash_sat_10_09.smt2 new file mode 100644 index 000000000..20cff8b1b --- /dev/null +++ b/test/regress/regress1/hash_sat_10_09.smt2 @@ -0,0 +1,27 @@ +(set-logic QF_UFLIA) +(set-info :source | MathSat group |) +(set-info :smt-lib-version 2.0) +(set-info :category "crafted") +(set-info :status sat) +(declare-fun hash_1 (Int) Int) +(declare-fun hash_2 (Int) Int) +(declare-fun hash_3 (Int) Int) +(declare-fun hash_4 (Int) Int) +(declare-fun hash_5 (Int) Int) +(declare-fun hash_6 (Int) Int) +(declare-fun hash_7 (Int) Int) +(declare-fun hash_8 (Int) Int) +(declare-fun hash_9 (Int) Int) +(declare-fun x1 () Int) +(declare-fun x2 () Int) +(declare-fun x3 () Int) +(declare-fun x4 () Int) +(declare-fun x5 () Int) +(declare-fun x6 () Int) +(declare-fun x7 () Int) +(declare-fun x8 () Int) +(declare-fun x9 () Int) +(declare-fun x10 () Int) +(assert (let ((?v_0 (hash_1 x1)) (?v_1 (hash_1 x2)) (?v_2 (hash_1 x3)) (?v_3 (hash_1 x4)) (?v_4 (hash_1 x5)) (?v_5 (hash_1 x6)) (?v_6 (hash_1 x7)) (?v_7 (hash_1 x8)) (?v_8 (hash_1 x9)) (?v_9 (hash_1 x10)) (?v_10 (hash_2 x1)) (?v_11 (hash_2 x2)) (?v_12 (hash_2 x3)) (?v_13 (hash_2 x4)) (?v_14 (hash_2 x5)) (?v_15 (hash_2 x6)) (?v_16 (hash_2 x7)) (?v_17 (hash_2 x8)) (?v_18 (hash_2 x9)) (?v_19 (hash_2 x10)) (?v_20 (hash_3 x1)) (?v_21 (hash_3 x2)) (?v_22 (hash_3 x3)) (?v_23 (hash_3 x4)) (?v_24 (hash_3 x5)) (?v_25 (hash_3 x6)) (?v_26 (hash_3 x7)) (?v_27 (hash_3 x8)) (?v_28 (hash_3 x9)) (?v_29 (hash_3 x10)) (?v_30 (hash_4 x1)) (?v_31 (hash_4 x2)) (?v_32 (hash_4 x3)) (?v_33 (hash_4 x4)) (?v_34 (hash_4 x5)) (?v_35 (hash_4 x6)) (?v_36 (hash_4 x7)) (?v_37 (hash_4 x8)) (?v_38 (hash_4 x9)) (?v_39 (hash_4 x10)) (?v_40 (hash_5 x1)) (?v_41 (hash_5 x2)) (?v_42 (hash_5 x3)) (?v_43 (hash_5 x4)) (?v_44 (hash_5 x5)) (?v_45 (hash_5 x6)) (?v_46 (hash_5 x7)) (?v_47 (hash_5 x8)) (?v_48 (hash_5 x9)) (?v_49 (hash_5 x10)) (?v_50 (hash_6 x1)) (?v_51 (hash_6 x2)) (?v_52 (hash_6 x3)) (?v_53 (hash_6 x4)) (?v_54 (hash_6 x5)) (?v_55 (hash_6 x6)) (?v_56 (hash_6 x7)) (?v_57 (hash_6 x8)) (?v_58 (hash_6 x9)) (?v_59 (hash_6 x10)) (?v_60 (hash_7 x1)) (?v_61 (hash_7 x2)) (?v_62 (hash_7 x3)) (?v_63 (hash_7 x4)) (?v_64 (hash_7 x5)) (?v_65 (hash_7 x6)) (?v_66 (hash_7 x7)) (?v_67 (hash_7 x8)) (?v_68 (hash_7 x9)) (?v_69 (hash_7 x10)) (?v_70 (hash_8 x1)) (?v_71 (hash_8 x2)) (?v_72 (hash_8 x3)) (?v_73 (hash_8 x4)) (?v_74 (hash_8 x5)) (?v_75 (hash_8 x6)) (?v_76 (hash_8 x7)) (?v_77 (hash_8 x8)) (?v_78 (hash_8 x9)) (?v_79 (hash_8 x10)) (?v_80 (hash_9 x1)) (?v_81 (hash_9 x2)) (?v_82 (hash_9 x3)) (?v_83 (hash_9 x4)) (?v_84 (hash_9 x5)) (?v_85 (hash_9 x6)) (?v_86 (hash_9 x7)) (?v_87 (hash_9 x8)) (?v_88 (hash_9 x9)) (?v_89 (hash_9 x10)) (?v_90 (+ x1 x10)) (?v_91 (+ x1 x2))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (distinct ?v_0 ?v_1) (distinct ?v_0 ?v_2)) (distinct ?v_0 ?v_3)) (distinct ?v_0 ?v_4)) (distinct ?v_0 ?v_5)) (distinct ?v_0 ?v_6)) (distinct ?v_0 ?v_7)) (distinct ?v_0 ?v_8)) (distinct ?v_0 ?v_9)) (distinct ?v_1 ?v_2)) (distinct ?v_1 ?v_3)) (distinct ?v_1 ?v_4)) (distinct ?v_1 ?v_5)) (distinct ?v_1 ?v_6)) (distinct ?v_1 ?v_7)) (distinct ?v_1 ?v_8)) (distinct ?v_1 ?v_9)) (distinct ?v_2 ?v_3)) (distinct ?v_2 ?v_4)) (distinct ?v_2 ?v_5)) (distinct ?v_2 ?v_6)) (distinct ?v_2 ?v_7)) (distinct ?v_2 ?v_8)) (distinct ?v_2 ?v_9)) (distinct ?v_3 ?v_4)) (distinct ?v_3 ?v_5)) (distinct ?v_3 ?v_6)) (distinct ?v_3 ?v_7)) (distinct ?v_3 ?v_8)) (distinct ?v_3 ?v_9)) (distinct ?v_4 ?v_5)) (distinct ?v_4 ?v_6)) (distinct ?v_4 ?v_7)) (distinct ?v_4 ?v_8)) (distinct ?v_4 ?v_9)) (distinct ?v_5 ?v_6)) (distinct ?v_5 ?v_7)) (distinct ?v_5 ?v_8)) (distinct ?v_5 ?v_9)) (distinct ?v_6 ?v_7)) (distinct ?v_6 ?v_8)) (distinct ?v_6 ?v_9)) (distinct ?v_7 ?v_8)) (distinct ?v_7 ?v_9)) (distinct ?v_8 ?v_9)) (distinct ?v_10 ?v_11)) (distinct ?v_10 ?v_12)) (distinct ?v_10 ?v_13)) (distinct ?v_10 ?v_14)) (distinct ?v_10 ?v_15)) (distinct ?v_10 ?v_16)) (distinct ?v_10 ?v_17)) (distinct ?v_10 ?v_18)) (distinct ?v_10 ?v_19)) (distinct ?v_11 ?v_12)) (distinct ?v_11 ?v_13)) (distinct ?v_11 ?v_14)) (distinct ?v_11 ?v_15)) (distinct ?v_11 ?v_16)) (distinct ?v_11 ?v_17)) (distinct ?v_11 ?v_18)) (distinct ?v_11 ?v_19)) (distinct ?v_12 ?v_13)) (distinct ?v_12 ?v_14)) (distinct ?v_12 ?v_15)) (distinct ?v_12 ?v_16)) (distinct ?v_12 ?v_17)) (distinct ?v_12 ?v_18)) (distinct ?v_12 ?v_19)) (distinct ?v_13 ?v_14)) (distinct ?v_13 ?v_15)) (distinct ?v_13 ?v_16)) (distinct ?v_13 ?v_17)) (distinct ?v_13 ?v_18)) (distinct ?v_13 ?v_19)) (distinct ?v_14 ?v_15)) (distinct ?v_14 ?v_16)) (distinct ?v_14 ?v_17)) (distinct ?v_14 ?v_18)) (distinct ?v_14 ?v_19)) (distinct ?v_15 ?v_16)) (distinct ?v_15 ?v_17)) (distinct ?v_15 ?v_18)) (distinct ?v_15 ?v_19)) (distinct ?v_16 ?v_17)) (distinct ?v_16 ?v_18)) (distinct ?v_16 ?v_19)) (distinct ?v_17 ?v_18)) (distinct ?v_17 ?v_19)) (distinct ?v_18 ?v_19)) (distinct ?v_20 ?v_21)) (distinct ?v_20 ?v_22)) (distinct ?v_20 ?v_23)) (distinct ?v_20 ?v_24)) (distinct ?v_20 ?v_25)) (distinct ?v_20 ?v_26)) (distinct ?v_20 ?v_27)) (distinct ?v_20 ?v_28)) (distinct ?v_20 ?v_29)) (distinct ?v_21 ?v_22)) (distinct ?v_21 ?v_23)) (distinct ?v_21 ?v_24)) (distinct ?v_21 ?v_25)) (distinct ?v_21 ?v_26)) (distinct ?v_21 ?v_27)) (distinct ?v_21 ?v_28)) (distinct ?v_21 ?v_29)) (distinct ?v_22 ?v_23)) (distinct ?v_22 ?v_24)) (distinct ?v_22 ?v_25)) (distinct ?v_22 ?v_26)) (distinct ?v_22 ?v_27)) (distinct ?v_22 ?v_28)) (distinct ?v_22 ?v_29)) (distinct ?v_23 ?v_24)) (distinct ?v_23 ?v_25)) (distinct ?v_23 ?v_26)) (distinct ?v_23 ?v_27)) (distinct ?v_23 ?v_28)) (distinct ?v_23 ?v_29)) (distinct ?v_24 ?v_25)) (distinct ?v_24 ?v_26)) (distinct ?v_24 ?v_27)) (distinct ?v_24 ?v_28)) (distinct ?v_24 ?v_29)) (distinct ?v_25 ?v_26)) (distinct ?v_25 ?v_27)) (distinct ?v_25 ?v_28)) (distinct ?v_25 ?v_29)) (distinct ?v_26 ?v_27)) (distinct ?v_26 ?v_28)) (distinct ?v_26 ?v_29)) (distinct ?v_27 ?v_28)) (distinct ?v_27 ?v_29)) (distinct ?v_28 ?v_29)) (distinct ?v_30 ?v_31)) (distinct ?v_30 ?v_32)) (distinct ?v_30 ?v_33)) (distinct ?v_30 ?v_34)) (distinct ?v_30 ?v_35)) (distinct ?v_30 ?v_36)) (distinct ?v_30 ?v_37)) (distinct ?v_30 ?v_38)) (distinct ?v_30 ?v_39)) (distinct ?v_31 ?v_32)) (distinct ?v_31 ?v_33)) (distinct ?v_31 ?v_34)) (distinct ?v_31 ?v_35)) (distinct ?v_31 ?v_36)) (distinct ?v_31 ?v_37)) (distinct ?v_31 ?v_38)) (distinct ?v_31 ?v_39)) (distinct ?v_32 ?v_33)) (distinct ?v_32 ?v_34)) (distinct ?v_32 ?v_35)) (distinct ?v_32 ?v_36)) (distinct ?v_32 ?v_37)) (distinct ?v_32 ?v_38)) (distinct ?v_32 ?v_39)) (distinct ?v_33 ?v_34)) (distinct ?v_33 ?v_35)) (distinct ?v_33 ?v_36)) (distinct ?v_33 ?v_37)) (distinct ?v_33 ?v_38)) (distinct ?v_33 ?v_39)) (distinct ?v_34 ?v_35)) (distinct ?v_34 ?v_36)) (distinct ?v_34 ?v_37)) (distinct ?v_34 ?v_38)) (distinct ?v_34 ?v_39)) (distinct ?v_35 ?v_36)) (distinct ?v_35 ?v_37)) (distinct ?v_35 ?v_38)) (distinct ?v_35 ?v_39)) (distinct ?v_36 ?v_37)) (distinct ?v_36 ?v_38)) (distinct ?v_36 ?v_39)) (distinct ?v_37 ?v_38)) (distinct ?v_37 ?v_39)) (distinct ?v_38 ?v_39)) (distinct ?v_40 ?v_41)) (distinct ?v_40 ?v_42)) (distinct ?v_40 ?v_43)) (distinct ?v_40 ?v_44)) (distinct ?v_40 ?v_45)) (distinct ?v_40 ?v_46)) (distinct ?v_40 ?v_47)) (distinct ?v_40 ?v_48)) (distinct ?v_40 ?v_49)) (distinct ?v_41 ?v_42)) (distinct ?v_41 ?v_43)) (distinct ?v_41 ?v_44)) (distinct ?v_41 ?v_45)) (distinct ?v_41 ?v_46)) (distinct ?v_41 ?v_47)) (distinct ?v_41 ?v_48)) (distinct ?v_41 ?v_49)) (distinct ?v_42 ?v_43)) (distinct ?v_42 ?v_44)) (distinct ?v_42 ?v_45)) (distinct ?v_42 ?v_46)) (distinct ?v_42 ?v_47)) (distinct ?v_42 ?v_48)) (distinct ?v_42 ?v_49)) (distinct ?v_43 ?v_44)) (distinct ?v_43 ?v_45)) (distinct ?v_43 ?v_46)) (distinct ?v_43 ?v_47)) (distinct ?v_43 ?v_48)) (distinct ?v_43 ?v_49)) (distinct ?v_44 ?v_45)) (distinct ?v_44 ?v_46)) (distinct ?v_44 ?v_47)) (distinct ?v_44 ?v_48)) (distinct ?v_44 ?v_49)) (distinct ?v_45 ?v_46)) (distinct ?v_45 ?v_47)) (distinct ?v_45 ?v_48)) (distinct ?v_45 ?v_49)) (distinct ?v_46 ?v_47)) (distinct ?v_46 ?v_48)) (distinct ?v_46 ?v_49)) (distinct ?v_47 ?v_48)) (distinct ?v_47 ?v_49)) (distinct ?v_48 ?v_49)) (distinct ?v_50 ?v_51)) (distinct ?v_50 ?v_52)) (distinct ?v_50 ?v_53)) (distinct ?v_50 ?v_54)) (distinct ?v_50 ?v_55)) (distinct ?v_50 ?v_56)) (distinct ?v_50 ?v_57)) (distinct ?v_50 ?v_58)) (distinct ?v_50 ?v_59)) (distinct ?v_51 ?v_52)) (distinct ?v_51 ?v_53)) (distinct ?v_51 ?v_54)) (distinct ?v_51 ?v_55)) (distinct ?v_51 ?v_56)) (distinct ?v_51 ?v_57)) (distinct ?v_51 ?v_58)) (distinct ?v_51 ?v_59)) (distinct ?v_52 ?v_53)) (distinct ?v_52 ?v_54)) (distinct ?v_52 ?v_55)) (distinct ?v_52 ?v_56)) (distinct ?v_52 ?v_57)) (distinct ?v_52 ?v_58)) (distinct ?v_52 ?v_59)) (distinct ?v_53 ?v_54)) (distinct ?v_53 ?v_55)) (distinct ?v_53 ?v_56)) (distinct ?v_53 ?v_57)) (distinct ?v_53 ?v_58)) (distinct ?v_53 ?v_59)) (distinct ?v_54 ?v_55)) (distinct ?v_54 ?v_56)) (distinct ?v_54 ?v_57)) (distinct ?v_54 ?v_58)) (distinct ?v_54 ?v_59)) (distinct ?v_55 ?v_56)) (distinct ?v_55 ?v_57)) (distinct ?v_55 ?v_58)) (distinct ?v_55 ?v_59)) (distinct ?v_56 ?v_57)) (distinct ?v_56 ?v_58)) (distinct ?v_56 ?v_59)) (distinct ?v_57 ?v_58)) (distinct ?v_57 ?v_59)) (distinct ?v_58 ?v_59)) (distinct ?v_60 ?v_61)) (distinct ?v_60 ?v_62)) (distinct ?v_60 ?v_63)) (distinct ?v_60 ?v_64)) (distinct ?v_60 ?v_65)) (distinct ?v_60 ?v_66)) (distinct ?v_60 ?v_67)) (distinct ?v_60 ?v_68)) (distinct ?v_60 ?v_69)) (distinct ?v_61 ?v_62)) (distinct ?v_61 ?v_63)) (distinct ?v_61 ?v_64)) (distinct ?v_61 ?v_65)) (distinct ?v_61 ?v_66)) (distinct ?v_61 ?v_67)) (distinct ?v_61 ?v_68)) (distinct ?v_61 ?v_69)) (distinct ?v_62 ?v_63)) (distinct ?v_62 ?v_64)) (distinct ?v_62 ?v_65)) (distinct ?v_62 ?v_66)) (distinct ?v_62 ?v_67)) (distinct ?v_62 ?v_68)) (distinct ?v_62 ?v_69)) (distinct ?v_63 ?v_64)) (distinct ?v_63 ?v_65)) (distinct ?v_63 ?v_66)) (distinct ?v_63 ?v_67)) (distinct ?v_63 ?v_68)) (distinct ?v_63 ?v_69)) (distinct ?v_64 ?v_65)) (distinct ?v_64 ?v_66)) (distinct ?v_64 ?v_67)) (distinct ?v_64 ?v_68)) (distinct ?v_64 ?v_69)) (distinct ?v_65 ?v_66)) (distinct ?v_65 ?v_67)) (distinct ?v_65 ?v_68)) (distinct ?v_65 ?v_69)) (distinct ?v_66 ?v_67)) (distinct ?v_66 ?v_68)) (distinct ?v_66 ?v_69)) (distinct ?v_67 ?v_68)) (distinct ?v_67 ?v_69)) (distinct ?v_68 ?v_69)) (distinct ?v_70 ?v_71)) (distinct ?v_70 ?v_72)) (distinct ?v_70 ?v_73)) (distinct ?v_70 ?v_74)) (distinct ?v_70 ?v_75)) (distinct ?v_70 ?v_76)) (distinct ?v_70 ?v_77)) (distinct ?v_70 ?v_78)) (distinct ?v_70 ?v_79)) (distinct ?v_71 ?v_72)) (distinct ?v_71 ?v_73)) (distinct ?v_71 ?v_74)) (distinct ?v_71 ?v_75)) (distinct ?v_71 ?v_76)) (distinct ?v_71 ?v_77)) (distinct ?v_71 ?v_78)) (distinct ?v_71 ?v_79)) (distinct ?v_72 ?v_73)) (distinct ?v_72 ?v_74)) (distinct ?v_72 ?v_75)) (distinct ?v_72 ?v_76)) (distinct ?v_72 ?v_77)) (distinct ?v_72 ?v_78)) (distinct ?v_72 ?v_79)) (distinct ?v_73 ?v_74)) (distinct ?v_73 ?v_75)) (distinct ?v_73 ?v_76)) (distinct ?v_73 ?v_77)) (distinct ?v_73 ?v_78)) (distinct ?v_73 ?v_79)) (distinct ?v_74 ?v_75)) (distinct ?v_74 ?v_76)) (distinct ?v_74 ?v_77)) (distinct ?v_74 ?v_78)) (distinct ?v_74 ?v_79)) (distinct ?v_75 ?v_76)) (distinct ?v_75 ?v_77)) (distinct ?v_75 ?v_78)) (distinct ?v_75 ?v_79)) (distinct ?v_76 ?v_77)) (distinct ?v_76 ?v_78)) (distinct ?v_76 ?v_79)) (distinct ?v_77 ?v_78)) (distinct ?v_77 ?v_79)) (distinct ?v_78 ?v_79)) (distinct ?v_80 ?v_81)) (distinct ?v_80 ?v_82)) (distinct ?v_80 ?v_83)) (distinct ?v_80 ?v_84)) (distinct ?v_80 ?v_85)) (distinct ?v_80 ?v_86)) (distinct ?v_80 ?v_87)) (distinct ?v_80 ?v_88)) (distinct ?v_80 ?v_89)) (distinct ?v_81 ?v_82)) (distinct ?v_81 ?v_83)) (distinct ?v_81 ?v_84)) (distinct ?v_81 ?v_85)) (distinct ?v_81 ?v_86)) (distinct ?v_81 ?v_87)) (distinct ?v_81 ?v_88)) (distinct ?v_81 ?v_89)) (distinct ?v_82 ?v_83)) (distinct ?v_82 ?v_84)) (distinct ?v_82 ?v_85)) (distinct ?v_82 ?v_86)) (distinct ?v_82 ?v_87)) (distinct ?v_82 ?v_88)) (distinct ?v_82 ?v_89)) (distinct ?v_83 ?v_84)) (distinct ?v_83 ?v_85)) (distinct ?v_83 ?v_86)) (distinct ?v_83 ?v_87)) (distinct ?v_83 ?v_88)) (distinct ?v_83 ?v_89)) (distinct ?v_84 ?v_85)) (distinct ?v_84 ?v_86)) (distinct ?v_84 ?v_87)) (distinct ?v_84 ?v_88)) (distinct ?v_84 ?v_89)) (distinct ?v_85 ?v_86)) (distinct ?v_85 ?v_87)) (distinct ?v_85 ?v_88)) (distinct ?v_85 ?v_89)) (distinct ?v_86 ?v_87)) (distinct ?v_86 ?v_88)) (distinct ?v_86 ?v_89)) (distinct ?v_87 ?v_88)) (distinct ?v_87 ?v_89)) (distinct ?v_88 ?v_89)) (or (or (or (or (or (or (or (or (or (= ?v_0 x1) (= ?v_0 x2)) (= ?v_0 x3)) (= ?v_0 x4)) (= ?v_0 x5)) (= ?v_0 x6)) (= ?v_0 x7)) (= ?v_0 x8)) (= ?v_0 x9)) (= ?v_0 x10))) (or (or (or (or (or (or (or (or (or (= ?v_1 x1) (= ?v_1 x2)) (= ?v_1 x3)) (= ?v_1 x4)) (= ?v_1 x5)) (= ?v_1 x6)) (= ?v_1 x7)) (= ?v_1 x8)) (= ?v_1 x9)) (= ?v_1 x10))) (or (or (or (or (or (or (or (or (or (= ?v_2 x1) (= ?v_2 x2)) (= ?v_2 x3)) (= ?v_2 x4)) (= ?v_2 x5)) (= ?v_2 x6)) (= ?v_2 x7)) (= ?v_2 x8)) (= ?v_2 x9)) (= ?v_2 x10))) (or (or (or (or (or (or (or (or (or (= ?v_3 x1) (= ?v_3 x2)) (= ?v_3 x3)) (= ?v_3 x4)) (= ?v_3 x5)) (= ?v_3 x6)) (= ?v_3 x7)) (= ?v_3 x8)) (= ?v_3 x9)) (= ?v_3 x10))) (or (or (or (or (or (or (or (or (or (= ?v_4 x1) (= ?v_4 x2)) (= ?v_4 x3)) (= ?v_4 x4)) (= ?v_4 x5)) (= ?v_4 x6)) (= ?v_4 x7)) (= ?v_4 x8)) (= ?v_4 x9)) (= ?v_4 x10))) (or (or (or (or (or (or (or (or (or (= ?v_5 x1) (= ?v_5 x2)) (= ?v_5 x3)) (= ?v_5 x4)) (= ?v_5 x5)) (= ?v_5 x6)) (= ?v_5 x7)) (= ?v_5 x8)) (= ?v_5 x9)) (= ?v_5 x10))) (or (or (or (or (or (or (or (or (or (= ?v_6 x1) (= ?v_6 x2)) (= ?v_6 x3)) (= ?v_6 x4)) (= ?v_6 x5)) (= ?v_6 x6)) (= ?v_6 x7)) (= ?v_6 x8)) (= ?v_6 x9)) (= ?v_6 x10))) (or (or (or (or (or (or (or (or (or (= ?v_7 x1) (= ?v_7 x2)) (= ?v_7 x3)) (= ?v_7 x4)) (= ?v_7 x5)) (= ?v_7 x6)) (= ?v_7 x7)) (= ?v_7 x8)) (= ?v_7 x9)) (= ?v_7 x10))) (or (or (or (or (or (or (or (or (or (= ?v_8 x1) (= ?v_8 x2)) (= ?v_8 x3)) (= ?v_8 x4)) (= ?v_8 x5)) (= ?v_8 x6)) (= ?v_8 x7)) (= ?v_8 x8)) (= ?v_8 x9)) (= ?v_8 x10))) (or (or (or (or (or (or (or (or (or (= ?v_9 x1) (= ?v_9 x2)) (= ?v_9 x3)) (= ?v_9 x4)) (= ?v_9 x5)) (= ?v_9 x6)) (= ?v_9 x7)) (= ?v_9 x8)) (= ?v_9 x9)) (= ?v_9 x10))) (or (or (or (or (or (or (or (or (or (= ?v_10 x1) (= ?v_10 x2)) (= ?v_10 x3)) (= ?v_10 x4)) (= ?v_10 x5)) (= ?v_10 x6)) (= ?v_10 x7)) (= ?v_10 x8)) (= ?v_10 x9)) (= ?v_10 x10))) (or (or (or (or (or (or (or (or (or (= ?v_11 x1) (= ?v_11 x2)) (= ?v_11 x3)) (= ?v_11 x4)) (= ?v_11 x5)) (= ?v_11 x6)) (= ?v_11 x7)) (= ?v_11 x8)) (= ?v_11 x9)) (= ?v_11 x10))) (or (or (or (or (or (or (or (or (or (= ?v_12 x1) (= ?v_12 x2)) (= ?v_12 x3)) (= ?v_12 x4)) (= ?v_12 x5)) (= ?v_12 x6)) (= ?v_12 x7)) (= ?v_12 x8)) (= ?v_12 x9)) (= ?v_12 x10))) (or (or (or (or (or (or (or (or (or (= ?v_13 x1) (= ?v_13 x2)) (= ?v_13 x3)) (= ?v_13 x4)) (= ?v_13 x5)) (= ?v_13 x6)) (= ?v_13 x7)) (= ?v_13 x8)) (= ?v_13 x9)) (= ?v_13 x10))) (or (or (or (or (or (or (or (or (or (= ?v_14 x1) (= ?v_14 x2)) (= ?v_14 x3)) (= ?v_14 x4)) (= ?v_14 x5)) (= ?v_14 x6)) (= ?v_14 x7)) (= ?v_14 x8)) (= ?v_14 x9)) (= ?v_14 x10))) (or (or (or (or (or (or (or (or (or (= ?v_15 x1) (= ?v_15 x2)) (= ?v_15 x3)) (= ?v_15 x4)) (= ?v_15 x5)) (= ?v_15 x6)) (= ?v_15 x7)) (= ?v_15 x8)) (= ?v_15 x9)) (= ?v_15 x10))) (or (or (or (or (or (or (or (or (or (= ?v_16 x1) (= ?v_16 x2)) (= ?v_16 x3)) (= ?v_16 x4)) (= ?v_16 x5)) (= ?v_16 x6)) (= ?v_16 x7)) (= ?v_16 x8)) (= ?v_16 x9)) (= ?v_16 x10))) (or (or (or (or (or (or (or (or (or (= ?v_17 x1) (= ?v_17 x2)) (= ?v_17 x3)) (= ?v_17 x4)) (= ?v_17 x5)) (= ?v_17 x6)) (= ?v_17 x7)) (= ?v_17 x8)) (= ?v_17 x9)) (= ?v_17 x10))) (or (or (or (or (or (or (or (or (or (= ?v_18 x1) (= ?v_18 x2)) (= ?v_18 x3)) (= ?v_18 x4)) (= ?v_18 x5)) (= ?v_18 x6)) (= ?v_18 x7)) (= ?v_18 x8)) (= ?v_18 x9)) (= ?v_18 x10))) (or (or (or (or (or (or (or (or (or (= ?v_19 x1) (= ?v_19 x2)) (= ?v_19 x3)) (= ?v_19 x4)) (= ?v_19 x5)) (= ?v_19 x6)) (= ?v_19 x7)) (= ?v_19 x8)) (= ?v_19 x9)) (= ?v_19 x10))) (or (or (or (or (or (or (or (or (or (= ?v_20 x1) (= ?v_20 x2)) (= ?v_20 x3)) (= ?v_20 x4)) (= ?v_20 x5)) (= ?v_20 x6)) (= ?v_20 x7)) (= ?v_20 x8)) (= ?v_20 x9)) (= ?v_20 x10))) (or (or (or (or (or (or (or (or (or (= ?v_21 x1) (= ?v_21 x2)) (= ?v_21 x3)) (= ?v_21 x4)) (= ?v_21 x5)) (= ?v_21 x6)) (= ?v_21 x7)) (= ?v_21 x8)) (= ?v_21 x9)) (= ?v_21 x10))) (or (or (or (or (or (or (or (or (or (= ?v_22 x1) (= ?v_22 x2)) (= ?v_22 x3)) (= ?v_22 x4)) (= ?v_22 x5)) (= ?v_22 x6)) (= ?v_22 x7)) (= ?v_22 x8)) (= ?v_22 x9)) (= ?v_22 x10))) (or (or (or (or (or (or (or (or (or (= ?v_23 x1) (= ?v_23 x2)) (= ?v_23 x3)) (= ?v_23 x4)) (= ?v_23 x5)) (= ?v_23 x6)) (= ?v_23 x7)) (= ?v_23 x8)) (= ?v_23 x9)) (= ?v_23 x10))) (or (or (or (or (or (or (or (or (or (= ?v_24 x1) (= ?v_24 x2)) (= ?v_24 x3)) (= ?v_24 x4)) (= ?v_24 x5)) (= ?v_24 x6)) (= ?v_24 x7)) (= ?v_24 x8)) (= ?v_24 x9)) (= ?v_24 x10))) (or (or (or (or (or (or (or (or (or (= ?v_25 x1) (= ?v_25 x2)) (= ?v_25 x3)) (= ?v_25 x4)) (= ?v_25 x5)) (= ?v_25 x6)) (= ?v_25 x7)) (= ?v_25 x8)) (= ?v_25 x9)) (= ?v_25 x10))) (or (or (or (or (or (or (or (or (or (= ?v_26 x1) (= ?v_26 x2)) (= ?v_26 x3)) (= ?v_26 x4)) (= ?v_26 x5)) (= ?v_26 x6)) (= ?v_26 x7)) (= ?v_26 x8)) (= ?v_26 x9)) (= ?v_26 x10))) (or (or (or (or (or (or (or (or (or (= ?v_27 x1) (= ?v_27 x2)) (= ?v_27 x3)) (= ?v_27 x4)) (= ?v_27 x5)) (= ?v_27 x6)) (= ?v_27 x7)) (= ?v_27 x8)) (= ?v_27 x9)) (= ?v_27 x10))) (or (or (or (or (or (or (or (or (or (= ?v_28 x1) (= ?v_28 x2)) (= ?v_28 x3)) (= ?v_28 x4)) (= ?v_28 x5)) (= ?v_28 x6)) (= ?v_28 x7)) (= ?v_28 x8)) (= ?v_28 x9)) (= ?v_28 x10))) (or (or (or (or (or (or (or (or (or (= ?v_29 x1) (= ?v_29 x2)) (= ?v_29 x3)) (= ?v_29 x4)) (= ?v_29 x5)) (= ?v_29 x6)) (= ?v_29 x7)) (= ?v_29 x8)) (= ?v_29 x9)) (= ?v_29 x10))) (or (or (or (or (or (or (or (or (or (= ?v_30 x1) (= ?v_30 x2)) (= ?v_30 x3)) (= ?v_30 x4)) (= ?v_30 x5)) (= ?v_30 x6)) (= ?v_30 x7)) (= ?v_30 x8)) (= ?v_30 x9)) (= ?v_30 x10))) (or (or (or (or (or (or (or (or (or (= ?v_31 x1) (= ?v_31 x2)) (= ?v_31 x3)) (= ?v_31 x4)) (= ?v_31 x5)) (= ?v_31 x6)) (= ?v_31 x7)) (= ?v_31 x8)) (= ?v_31 x9)) (= ?v_31 x10))) (or (or (or (or (or (or (or (or (or (= ?v_32 x1) (= ?v_32 x2)) (= ?v_32 x3)) (= ?v_32 x4)) (= ?v_32 x5)) (= ?v_32 x6)) (= ?v_32 x7)) (= ?v_32 x8)) (= ?v_32 x9)) (= ?v_32 x10))) (or (or (or (or (or (or (or (or (or (= ?v_33 x1) (= ?v_33 x2)) (= ?v_33 x3)) (= ?v_33 x4)) (= ?v_33 x5)) (= ?v_33 x6)) (= ?v_33 x7)) (= ?v_33 x8)) (= ?v_33 x9)) (= ?v_33 x10))) (or (or (or (or (or (or (or (or (or (= ?v_34 x1) (= ?v_34 x2)) (= ?v_34 x3)) (= ?v_34 x4)) (= ?v_34 x5)) (= ?v_34 x6)) (= ?v_34 x7)) (= ?v_34 x8)) (= ?v_34 x9)) (= ?v_34 x10))) (or (or (or (or (or (or (or (or (or (= ?v_35 x1) (= ?v_35 x2)) (= ?v_35 x3)) (= ?v_35 x4)) (= ?v_35 x5)) (= ?v_35 x6)) (= ?v_35 x7)) (= ?v_35 x8)) (= ?v_35 x9)) (= ?v_35 x10))) (or (or (or (or (or (or (or (or (or (= ?v_36 x1) (= ?v_36 x2)) (= ?v_36 x3)) (= ?v_36 x4)) (= ?v_36 x5)) (= ?v_36 x6)) (= ?v_36 x7)) (= ?v_36 x8)) (= ?v_36 x9)) (= ?v_36 x10))) (or (or (or (or (or (or (or (or (or (= ?v_37 x1) (= ?v_37 x2)) (= ?v_37 x3)) (= ?v_37 x4)) (= ?v_37 x5)) (= ?v_37 x6)) (= ?v_37 x7)) (= ?v_37 x8)) (= ?v_37 x9)) (= ?v_37 x10))) (or (or (or (or (or (or (or (or (or (= ?v_38 x1) (= ?v_38 x2)) (= ?v_38 x3)) (= ?v_38 x4)) (= ?v_38 x5)) (= ?v_38 x6)) (= ?v_38 x7)) (= ?v_38 x8)) (= ?v_38 x9)) (= ?v_38 x10))) (or (or (or (or (or (or (or (or (or (= ?v_39 x1) (= ?v_39 x2)) (= ?v_39 x3)) (= ?v_39 x4)) (= ?v_39 x5)) (= ?v_39 x6)) (= ?v_39 x7)) (= ?v_39 x8)) (= ?v_39 x9)) (= ?v_39 x10))) (or (or (or (or (or (or (or (or (or (= ?v_40 x1) (= ?v_40 x2)) (= ?v_40 x3)) (= ?v_40 x4)) (= ?v_40 x5)) (= ?v_40 x6)) (= ?v_40 x7)) (= ?v_40 x8)) (= ?v_40 x9)) (= ?v_40 x10))) (or (or (or (or (or (or (or (or (or (= ?v_41 x1) (= ?v_41 x2)) (= ?v_41 x3)) (= ?v_41 x4)) (= ?v_41 x5)) (= ?v_41 x6)) (= ?v_41 x7)) (= ?v_41 x8)) (= ?v_41 x9)) (= ?v_41 x10))) (or (or (or (or (or (or (or (or (or (= ?v_42 x1) (= ?v_42 x2)) (= ?v_42 x3)) (= ?v_42 x4)) (= ?v_42 x5)) (= ?v_42 x6)) (= ?v_42 x7)) (= ?v_42 x8)) (= ?v_42 x9)) (= ?v_42 x10))) (or (or (or (or (or (or (or (or (or (= ?v_43 x1) (= ?v_43 x2)) (= ?v_43 x3)) (= ?v_43 x4)) (= ?v_43 x5)) (= ?v_43 x6)) (= ?v_43 x7)) (= ?v_43 x8)) (= ?v_43 x9)) (= ?v_43 x10))) (or (or (or (or (or (or (or (or (or (= ?v_44 x1) (= ?v_44 x2)) (= ?v_44 x3)) (= ?v_44 x4)) (= ?v_44 x5)) (= ?v_44 x6)) (= ?v_44 x7)) (= ?v_44 x8)) (= ?v_44 x9)) (= ?v_44 x10))) (or (or (or (or (or (or (or (or (or (= ?v_45 x1) (= ?v_45 x2)) (= ?v_45 x3)) (= ?v_45 x4)) (= ?v_45 x5)) (= ?v_45 x6)) (= ?v_45 x7)) (= ?v_45 x8)) (= ?v_45 x9)) (= ?v_45 x10))) (or (or (or (or (or (or (or (or (or (= ?v_46 x1) (= ?v_46 x2)) (= ?v_46 x3)) (= ?v_46 x4)) (= ?v_46 x5)) (= ?v_46 x6)) (= ?v_46 x7)) (= ?v_46 x8)) (= ?v_46 x9)) (= ?v_46 x10))) (or (or (or (or (or (or (or (or (or (= ?v_47 x1) (= ?v_47 x2)) (= ?v_47 x3)) (= ?v_47 x4)) (= ?v_47 x5)) (= ?v_47 x6)) (= ?v_47 x7)) (= ?v_47 x8)) (= ?v_47 x9)) (= ?v_47 x10))) (or (or (or (or (or (or (or (or (or (= ?v_48 x1) (= ?v_48 x2)) (= ?v_48 x3)) (= ?v_48 x4)) (= ?v_48 x5)) (= ?v_48 x6)) (= ?v_48 x7)) (= ?v_48 x8)) (= ?v_48 x9)) (= ?v_48 x10))) (or (or (or (or (or (or (or (or (or (= ?v_49 x1) (= ?v_49 x2)) (= ?v_49 x3)) (= ?v_49 x4)) (= ?v_49 x5)) (= ?v_49 x6)) (= ?v_49 x7)) (= ?v_49 x8)) (= ?v_49 x9)) (= ?v_49 x10))) (or (or (or (or (or (or (or (or (or (= ?v_50 x1) (= ?v_50 x2)) (= ?v_50 x3)) (= ?v_50 x4)) (= ?v_50 x5)) (= ?v_50 x6)) (= ?v_50 x7)) (= ?v_50 x8)) (= ?v_50 x9)) (= ?v_50 x10))) (or (or (or (or (or (or (or (or (or (= ?v_51 x1) (= ?v_51 x2)) (= ?v_51 x3)) (= ?v_51 x4)) (= ?v_51 x5)) (= ?v_51 x6)) (= ?v_51 x7)) (= ?v_51 x8)) (= ?v_51 x9)) (= ?v_51 x10))) (or (or (or (or (or (or (or (or (or (= ?v_52 x1) (= ?v_52 x2)) (= ?v_52 x3)) (= ?v_52 x4)) (= ?v_52 x5)) (= ?v_52 x6)) (= ?v_52 x7)) (= ?v_52 x8)) (= ?v_52 x9)) (= ?v_52 x10))) (or (or (or (or (or (or (or (or (or (= ?v_53 x1) (= ?v_53 x2)) (= ?v_53 x3)) (= ?v_53 x4)) (= ?v_53 x5)) (= ?v_53 x6)) (= ?v_53 x7)) (= ?v_53 x8)) (= ?v_53 x9)) (= ?v_53 x10))) (or (or (or (or (or (or (or (or (or (= ?v_54 x1) (= ?v_54 x2)) (= ?v_54 x3)) (= ?v_54 x4)) (= ?v_54 x5)) (= ?v_54 x6)) (= ?v_54 x7)) (= ?v_54 x8)) (= ?v_54 x9)) (= ?v_54 x10))) (or (or (or (or (or (or (or (or (or (= ?v_55 x1) (= ?v_55 x2)) (= ?v_55 x3)) (= ?v_55 x4)) (= ?v_55 x5)) (= ?v_55 x6)) (= ?v_55 x7)) (= ?v_55 x8)) (= ?v_55 x9)) (= ?v_55 x10))) (or (or (or (or (or (or (or (or (or (= ?v_56 x1) (= ?v_56 x2)) (= ?v_56 x3)) (= ?v_56 x4)) (= ?v_56 x5)) (= ?v_56 x6)) (= ?v_56 x7)) (= ?v_56 x8)) (= ?v_56 x9)) (= ?v_56 x10))) (or (or (or (or (or (or (or (or (or (= ?v_57 x1) (= ?v_57 x2)) (= ?v_57 x3)) (= ?v_57 x4)) (= ?v_57 x5)) (= ?v_57 x6)) (= ?v_57 x7)) (= ?v_57 x8)) (= ?v_57 x9)) (= ?v_57 x10))) (or (or (or (or (or (or (or (or (or (= ?v_58 x1) (= ?v_58 x2)) (= ?v_58 x3)) (= ?v_58 x4)) (= ?v_58 x5)) (= ?v_58 x6)) (= ?v_58 x7)) (= ?v_58 x8)) (= ?v_58 x9)) (= ?v_58 x10))) (or (or (or (or (or (or (or (or (or (= ?v_59 x1) (= ?v_59 x2)) (= ?v_59 x3)) (= ?v_59 x4)) (= ?v_59 x5)) (= ?v_59 x6)) (= ?v_59 x7)) (= ?v_59 x8)) (= ?v_59 x9)) (= ?v_59 x10))) (or (or (or (or (or (or (or (or (or (= ?v_60 x1) (= ?v_60 x2)) (= ?v_60 x3)) (= ?v_60 x4)) (= ?v_60 x5)) (= ?v_60 x6)) (= ?v_60 x7)) (= ?v_60 x8)) (= ?v_60 x9)) (= ?v_60 x10))) (or (or (or (or (or (or (or (or (or (= ?v_61 x1) (= ?v_61 x2)) (= ?v_61 x3)) (= ?v_61 x4)) (= ?v_61 x5)) (= ?v_61 x6)) (= ?v_61 x7)) (= ?v_61 x8)) (= ?v_61 x9)) (= ?v_61 x10))) (or (or (or (or (or (or (or (or (or (= ?v_62 x1) (= ?v_62 x2)) (= ?v_62 x3)) (= ?v_62 x4)) (= ?v_62 x5)) (= ?v_62 x6)) (= ?v_62 x7)) (= ?v_62 x8)) (= ?v_62 x9)) (= ?v_62 x10))) (or (or (or (or (or (or (or (or (or (= ?v_63 x1) (= ?v_63 x2)) (= ?v_63 x3)) (= ?v_63 x4)) (= ?v_63 x5)) (= ?v_63 x6)) (= ?v_63 x7)) (= ?v_63 x8)) (= ?v_63 x9)) (= ?v_63 x10))) (or (or (or (or (or (or (or (or (or (= ?v_64 x1) (= ?v_64 x2)) (= ?v_64 x3)) (= ?v_64 x4)) (= ?v_64 x5)) (= ?v_64 x6)) (= ?v_64 x7)) (= ?v_64 x8)) (= ?v_64 x9)) (= ?v_64 x10))) (or (or (or (or (or (or (or (or (or (= ?v_65 x1) (= ?v_65 x2)) (= ?v_65 x3)) (= ?v_65 x4)) (= ?v_65 x5)) (= ?v_65 x6)) (= ?v_65 x7)) (= ?v_65 x8)) (= ?v_65 x9)) (= ?v_65 x10))) (or (or (or (or (or (or (or (or (or (= ?v_66 x1) (= ?v_66 x2)) (= ?v_66 x3)) (= ?v_66 x4)) (= ?v_66 x5)) (= ?v_66 x6)) (= ?v_66 x7)) (= ?v_66 x8)) (= ?v_66 x9)) (= ?v_66 x10))) (or (or (or (or (or (or (or (or (or (= ?v_67 x1) (= ?v_67 x2)) (= ?v_67 x3)) (= ?v_67 x4)) (= ?v_67 x5)) (= ?v_67 x6)) (= ?v_67 x7)) (= ?v_67 x8)) (= ?v_67 x9)) (= ?v_67 x10))) (or (or (or (or (or (or (or (or (or (= ?v_68 x1) (= ?v_68 x2)) (= ?v_68 x3)) (= ?v_68 x4)) (= ?v_68 x5)) (= ?v_68 x6)) (= ?v_68 x7)) (= ?v_68 x8)) (= ?v_68 x9)) (= ?v_68 x10))) (or (or (or (or (or (or (or (or (or (= ?v_69 x1) (= ?v_69 x2)) (= ?v_69 x3)) (= ?v_69 x4)) (= ?v_69 x5)) (= ?v_69 x6)) (= ?v_69 x7)) (= ?v_69 x8)) (= ?v_69 x9)) (= ?v_69 x10))) (or (or (or (or (or (or (or (or (or (= ?v_70 x1) (= ?v_70 x2)) (= ?v_70 x3)) (= ?v_70 x4)) (= ?v_70 x5)) (= ?v_70 x6)) (= ?v_70 x7)) (= ?v_70 x8)) (= ?v_70 x9)) (= ?v_70 x10))) (or (or (or (or (or (or (or (or (or (= ?v_71 x1) (= ?v_71 x2)) (= ?v_71 x3)) (= ?v_71 x4)) (= ?v_71 x5)) (= ?v_71 x6)) (= ?v_71 x7)) (= ?v_71 x8)) (= ?v_71 x9)) (= ?v_71 x10))) (or (or (or (or (or (or (or (or (or (= ?v_72 x1) (= ?v_72 x2)) (= ?v_72 x3)) (= ?v_72 x4)) (= ?v_72 x5)) (= ?v_72 x6)) (= ?v_72 x7)) (= ?v_72 x8)) (= ?v_72 x9)) (= ?v_72 x10))) (or (or (or (or (or (or (or (or (or (= ?v_73 x1) (= ?v_73 x2)) (= ?v_73 x3)) (= ?v_73 x4)) (= ?v_73 x5)) (= ?v_73 x6)) (= ?v_73 x7)) (= ?v_73 x8)) (= ?v_73 x9)) (= ?v_73 x10))) (or (or (or (or (or (or (or (or (or (= ?v_74 x1) (= ?v_74 x2)) (= ?v_74 x3)) (= ?v_74 x4)) (= ?v_74 x5)) (= ?v_74 x6)) (= ?v_74 x7)) (= ?v_74 x8)) (= ?v_74 x9)) (= ?v_74 x10))) (or (or (or (or (or (or (or (or (or (= ?v_75 x1) (= ?v_75 x2)) (= ?v_75 x3)) (= ?v_75 x4)) (= ?v_75 x5)) (= ?v_75 x6)) (= ?v_75 x7)) (= ?v_75 x8)) (= ?v_75 x9)) (= ?v_75 x10))) (or (or (or (or (or (or (or (or (or (= ?v_76 x1) (= ?v_76 x2)) (= ?v_76 x3)) (= ?v_76 x4)) (= ?v_76 x5)) (= ?v_76 x6)) (= ?v_76 x7)) (= ?v_76 x8)) (= ?v_76 x9)) (= ?v_76 x10))) (or (or (or (or (or (or (or (or (or (= ?v_77 x1) (= ?v_77 x2)) (= ?v_77 x3)) (= ?v_77 x4)) (= ?v_77 x5)) (= ?v_77 x6)) (= ?v_77 x7)) (= ?v_77 x8)) (= ?v_77 x9)) (= ?v_77 x10))) (or (or (or (or (or (or (or (or (or (= ?v_78 x1) (= ?v_78 x2)) (= ?v_78 x3)) (= ?v_78 x4)) (= ?v_78 x5)) (= ?v_78 x6)) (= ?v_78 x7)) (= ?v_78 x8)) (= ?v_78 x9)) (= ?v_78 x10))) (or (or (or (or (or (or (or (or (or (= ?v_79 x1) (= ?v_79 x2)) (= ?v_79 x3)) (= ?v_79 x4)) (= ?v_79 x5)) (= ?v_79 x6)) (= ?v_79 x7)) (= ?v_79 x8)) (= ?v_79 x9)) (= ?v_79 x10))) (or (or (or (or (or (or (or (or (or (= ?v_80 x1) (= ?v_80 x2)) (= ?v_80 x3)) (= ?v_80 x4)) (= ?v_80 x5)) (= ?v_80 x6)) (= ?v_80 x7)) (= ?v_80 x8)) (= ?v_80 x9)) (= ?v_80 x10))) (or (or (or (or (or (or (or (or (or (= ?v_81 x1) (= ?v_81 x2)) (= ?v_81 x3)) (= ?v_81 x4)) (= ?v_81 x5)) (= ?v_81 x6)) (= ?v_81 x7)) (= ?v_81 x8)) (= ?v_81 x9)) (= ?v_81 x10))) (or (or (or (or (or (or (or (or (or (= ?v_82 x1) (= ?v_82 x2)) (= ?v_82 x3)) (= ?v_82 x4)) (= ?v_82 x5)) (= ?v_82 x6)) (= ?v_82 x7)) (= ?v_82 x8)) (= ?v_82 x9)) (= ?v_82 x10))) (or (or (or (or (or (or (or (or (or (= ?v_83 x1) (= ?v_83 x2)) (= ?v_83 x3)) (= ?v_83 x4)) (= ?v_83 x5)) (= ?v_83 x6)) (= ?v_83 x7)) (= ?v_83 x8)) (= ?v_83 x9)) (= ?v_83 x10))) (or (or (or (or (or (or (or (or (or (= ?v_84 x1) (= ?v_84 x2)) (= ?v_84 x3)) (= ?v_84 x4)) (= ?v_84 x5)) (= ?v_84 x6)) (= ?v_84 x7)) (= ?v_84 x8)) (= ?v_84 x9)) (= ?v_84 x10))) (or (or (or (or (or (or (or (or (or (= ?v_85 x1) (= ?v_85 x2)) (= ?v_85 x3)) (= ?v_85 x4)) (= ?v_85 x5)) (= ?v_85 x6)) (= ?v_85 x7)) (= ?v_85 x8)) (= ?v_85 x9)) (= ?v_85 x10))) (or (or (or (or (or (or (or (or (or (= ?v_86 x1) (= ?v_86 x2)) (= ?v_86 x3)) (= ?v_86 x4)) (= ?v_86 x5)) (= ?v_86 x6)) (= ?v_86 x7)) (= ?v_86 x8)) (= ?v_86 x9)) (= ?v_86 x10))) (or (or (or (or (or (or (or (or (or (= ?v_87 x1) (= ?v_87 x2)) (= ?v_87 x3)) (= ?v_87 x4)) (= ?v_87 x5)) (= ?v_87 x6)) (= ?v_87 x7)) (= ?v_87 x8)) (= ?v_87 x9)) (= ?v_87 x10))) (or (or (or (or (or (or (or (or (or (= ?v_88 x1) (= ?v_88 x2)) (= ?v_88 x3)) (= ?v_88 x4)) (= ?v_88 x5)) (= ?v_88 x6)) (= ?v_88 x7)) (= ?v_88 x8)) (= ?v_88 x9)) (= ?v_88 x10))) (or (or (or (or (or (or (or (or (or (= ?v_89 x1) (= ?v_89 x2)) (= ?v_89 x3)) (= ?v_89 x4)) (= ?v_89 x5)) (= ?v_89 x6)) (= ?v_89 x7)) (= ?v_89 x8)) (= ?v_89 x9)) (= ?v_89 x10))) (distinct x1 x2)) (distinct x1 x3)) (distinct x1 x4)) (distinct x1 x5)) (distinct x1 x6)) (distinct x1 x7)) (distinct x1 x8)) (distinct x1 x9)) (distinct x1 x10)) (distinct x2 x3)) (distinct x2 x4)) (distinct x2 x5)) (distinct x2 x6)) (distinct x2 x7)) (distinct x2 x8)) (distinct x2 x9)) (distinct x2 x10)) (distinct x3 x4)) (distinct x3 x5)) (distinct x3 x6)) (distinct x3 x7)) (distinct x3 x8)) (distinct x3 x9)) (distinct x3 x10)) (distinct x4 x5)) (distinct x4 x6)) (distinct x4 x7)) (distinct x4 x8)) (distinct x4 x9)) (distinct x4 x10)) (distinct x5 x6)) (distinct x5 x7)) (distinct x5 x8)) (distinct x5 x9)) (distinct x5 x10)) (distinct x6 x7)) (distinct x6 x8)) (distinct x6 x9)) (distinct x6 x10)) (distinct x7 x8)) (distinct x7 x9)) (distinct x7 x10)) (distinct x8 x9)) (distinct x8 x10)) (distinct x9 x10)) (<= 0 x1)) (< x1 11)) (<= 0 x2)) (< x2 11)) (<= 0 x3)) (< x3 11)) (<= 0 x4)) (< x4 11)) (<= 0 x5)) (< x5 11)) (<= 0 x6)) (< x6 11)) (<= 0 x7)) (< x7 11)) (<= 0 x8)) (< x8 11)) (<= 0 x9)) (< x9 11)) (<= 0 x10)) (< x10 11)) (= (hash_1 (hash_1 (hash_9 (ite (< ?v_90 11) ?v_90 x1)))) (hash_1 (hash_1 (hash_9 (ite (< ?v_91 11) ?v_91 x1)))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/ooo.tag10.smt2 b/test/regress/regress1/ooo.tag10.smt2 new file mode 100644 index 000000000..ef8e2244c --- /dev/null +++ b/test/regress/regress1/ooo.tag10.smt2 @@ -0,0 +1,28 @@ +(set-logic QF_UFIDL) +(set-info :source | +UCLID benchmark suite. See UCLID project: http://www.cs.cmu.edu/~uclid + +This benchmark was automatically translated into SMT-LIB format from +CVC format using CVC Lite +|) +(set-info :smt-lib-version 2.0) +(set-info :category "industrial") +(set-info :status unsat) +(declare-fun Br1 () Int) +(declare-fun Br2 () Int) +(declare-fun BOOOB_46_init_instr () Int) +(declare-fun BOOOB_46_init_rob_head () Int) +(declare-fun BOOOB_46_init_null_reg () Int) +(declare-fun BOOOB_46_init_n_oper_0 () Int) +(declare-fun BOOOB_46_init_n_oper_1 () Int) +(declare-fun BOOOB_46_New_ex_id (Int) Int) +(declare-fun BOOOB_46_New_var (Int) Int) +(declare-fun BOOOB_46_Decode_src2 (Int) Int) +(declare-fun BOOOB_46_Decode_src1 (Int) Int) +(declare-fun BOOOB_46_Decode_dest (Int) Int) +(declare-fun BOOOB_46_New_oper_1 (Int) Bool) +(declare-fun BOOOB_46_New_oper_0 (Int) Bool) +(declare-fun BOOOB_46_New_instr (Int) Int) +(assert (let ((?v_12 (BOOOB_46_New_var BOOOB_46_init_n_oper_1))) (let ((?v_10 (BOOOB_46_New_var ?v_12))) (let ((?v_8 (BOOOB_46_New_var ?v_10))) (let ((?v_6 (BOOOB_46_New_var ?v_8))) (let ((?v_4 (BOOOB_46_New_var ?v_6))) (let ((?v_2 (BOOOB_46_New_var ?v_4))) (let ((?v_0 (BOOOB_46_New_var ?v_2))) (let ((?v_21 (BOOOB_46_New_oper_1 (BOOOB_46_New_var ?v_0))) (?v_13 (BOOOB_46_New_var BOOOB_46_init_n_oper_0))) (let ((?v_11 (BOOOB_46_New_var ?v_13))) (let ((?v_9 (BOOOB_46_New_var ?v_11))) (let ((?v_7 (BOOOB_46_New_var ?v_9))) (let ((?v_5 (BOOOB_46_New_var ?v_7))) (let ((?v_3 (BOOOB_46_New_var ?v_5))) (let ((?v_1 (BOOOB_46_New_var ?v_3))) (let ((?v_22 (BOOOB_46_New_oper_0 (BOOOB_46_New_var ?v_1)))) (let ((?v_536 (and (not ?v_21) ?v_22)) (?v_23 (BOOOB_46_New_oper_1 ?v_0)) (?v_24 (BOOOB_46_New_oper_0 ?v_1))) (let ((?v_517 (and (not ?v_23) ?v_24)) (?v_25 (BOOOB_46_New_oper_1 ?v_2)) (?v_26 (BOOOB_46_New_oper_0 ?v_3))) (let ((?v_359 (and (not ?v_25) ?v_26)) (?v_27 (BOOOB_46_New_oper_1 ?v_4)) (?v_28 (BOOOB_46_New_oper_0 ?v_5))) (let ((?v_237 (and (not ?v_27) ?v_28)) (?v_29 (BOOOB_46_New_oper_1 ?v_6)) (?v_30 (BOOOB_46_New_oper_0 ?v_7))) (let ((?v_147 (and (not ?v_29) ?v_30)) (?v_31 (BOOOB_46_New_oper_1 ?v_8)) (?v_32 (BOOOB_46_New_oper_0 ?v_9))) (let ((?v_86 (and (not ?v_31) ?v_32)) (?v_33 (BOOOB_46_New_oper_1 ?v_10)) (?v_34 (BOOOB_46_New_oper_0 ?v_11))) (let ((?v_51 (and (not ?v_33) ?v_34)) (?v_35 (BOOOB_46_New_oper_1 ?v_12)) (?v_36 (BOOOB_46_New_oper_0 ?v_13))) (let ((?v_38 (and (not ?v_35) ?v_36)) (?v_37 (and (not (BOOOB_46_New_oper_1 BOOOB_46_init_n_oper_1)) (BOOOB_46_New_oper_0 BOOOB_46_init_n_oper_0)))) (let ((?v_14 (ite ?v_37 (BOOOB_46_New_instr BOOOB_46_init_instr) BOOOB_46_init_instr))) (let ((?v_15 (ite ?v_38 (BOOOB_46_New_instr ?v_14) ?v_14))) (let ((?v_16 (ite ?v_51 (BOOOB_46_New_instr ?v_15) ?v_15))) (let ((?v_17 (ite ?v_86 (BOOOB_46_New_instr ?v_16) ?v_16))) (let ((?v_18 (ite ?v_147 (BOOOB_46_New_instr ?v_17) ?v_17))) (let ((?v_19 (ite ?v_237 (BOOOB_46_New_instr ?v_18) ?v_18))) (let ((?v_20 (ite ?v_359 (BOOOB_46_New_instr ?v_19) ?v_19))) (let ((?v_537 (BOOOB_46_Decode_dest (ite ?v_517 (BOOOB_46_New_instr ?v_20) ?v_20)))) (let ((?v_555 (and ?v_536 (= ?v_537 Br1))) (?v_400 (and ?v_25 (not ?v_26))) (?v_415 (BOOOB_46_New_ex_id ?v_3)) (?v_513 (and ?v_25 ?v_26)) (?v_268 (and ?v_27 (not ?v_28))) (?v_280 (BOOOB_46_New_ex_id ?v_5)) (?v_355 (and ?v_27 ?v_28)) (?v_170 (and ?v_29 (not ?v_30))) (?v_179 (BOOOB_46_New_ex_id ?v_7)) (?v_233 (and ?v_29 ?v_30)) (?v_102 (and ?v_31 (not ?v_32))) (?v_108 (BOOOB_46_New_ex_id ?v_9)) (?v_143 (and ?v_31 ?v_32)) (?v_58 (and ?v_33 (not ?v_34))) (?v_63 (BOOOB_46_New_ex_id ?v_11)) (?v_82 (and ?v_33 ?v_34)) (?v_43 (and ?v_35 (not ?v_36))) (?v_48 (BOOOB_46_New_ex_id ?v_13))) (let ((?v_44 (= BOOOB_46_init_rob_head ?v_48))) (let ((?v_89 (and ?v_82 (and (and ?v_43 ?v_44) ?v_37))) (?v_40 (+ 1 BOOOB_46_init_rob_head))) (let ((?v_39 (ite ?v_37 ?v_40 BOOOB_46_init_rob_head))) (let ((?v_52 (ite ?v_38 (+ 1 ?v_39) ?v_39))) (let ((?v_83 (not (= BOOOB_46_init_rob_head ?v_52)))) (let ((?v_41 (ite (and ?v_89 ?v_83) ?v_40 BOOOB_46_init_rob_head))) (let ((?v_42 (and ?v_38 (= ?v_41 ?v_39))) (?v_46 (BOOOB_46_Decode_dest BOOOB_46_init_instr))) (let ((?v_59 (not (and ?v_37 (= ?v_46 (BOOOB_46_Decode_src1 ?v_14))))) (?v_49 (= ?v_41 BOOOB_46_init_rob_head))) (let ((?v_45 (and ?v_37 ?v_49)) (?v_61 (and ?v_37 ?v_44))) (let ((?v_47 (and (not ?v_42) (or (and ?v_43 (and (and (not ?v_45) ?v_44) ?v_61)) ?v_45))) (?v_67 (not (and ?v_37 (= ?v_46 (BOOOB_46_Decode_src2 ?v_14))))) (?v_50 (and (and ?v_43 (= ?v_48 ?v_41)) ?v_45)) (?v_69 (and ?v_35 ?v_36)) (?v_90 (= BOOOB_46_init_rob_head ?v_39))) (let ((?v_70 (not ?v_90))) (let ((?v_150 (and ?v_143 (or (and (and ?v_58 (= ?v_63 ?v_41)) (and (and (and (or (and ?v_42 ?v_59) ?v_47) (or (and ?v_42 ?v_67) ?v_47)) (not ?v_50)) (or ?v_42 (and (not (and (and ?v_69 ?v_49) ?v_70)) ?v_45)))) ?v_50))) (?v_87 (ite ?v_51 (+ 1 ?v_52) ?v_52))) (let ((?v_144 (not (= ?v_41 ?v_87)))) (let ((?v_53 (ite (and ?v_150 ?v_144) (+ 1 ?v_41) ?v_41))) (let ((?v_57 (and ?v_51 (= ?v_53 ?v_52))) (?v_72 (BOOOB_46_Decode_dest ?v_14)) (?v_54 (BOOOB_46_Decode_src1 ?v_15))) (let ((?v_55 (and ?v_38 (= ?v_72 ?v_54)))) (let ((?v_56 (ite ?v_55 ?v_39 BOOOB_46_init_rob_head))) (let ((?v_103 (or (and (not ?v_55) (not (and ?v_37 (= ?v_46 ?v_54)))) (and (and ?v_43 (= ?v_48 ?v_56)) (and ?v_37 (= ?v_56 BOOOB_46_init_rob_head))))) (?v_76 (not ?v_57)) (?v_60 (and ?v_38 (= ?v_53 ?v_39))) (?v_80 (= ?v_53 BOOOB_46_init_rob_head))) (let ((?v_62 (and ?v_37 ?v_80))) (let ((?v_77 (and (not ?v_60) (or (and ?v_43 (and (and (not ?v_62) ?v_44) ?v_61)) ?v_62)))) (let ((?v_71 (or (and ?v_60 ?v_59) ?v_77)) (?v_65 (= BOOOB_46_init_rob_head ?v_63)) (?v_64 (and ?v_38 (= ?v_63 ?v_39)))) (let ((?v_66 (and ?v_37 ?v_65))) (let ((?v_68 (and (not ?v_64) (or (and ?v_43 (and (and (not ?v_66) ?v_44) ?v_61)) ?v_66)))) (let ((?v_78 (and (and (and (or (and ?v_64 ?v_59) ?v_68) (or (and ?v_64 ?v_67) ?v_68)) (not (and (and ?v_43 (= ?v_48 ?v_63)) ?v_66))) (or ?v_64 (and (not (and (and ?v_69 ?v_65) ?v_70)) ?v_66)))) (?v_73 (BOOOB_46_Decode_src2 ?v_15))) (let ((?v_74 (and ?v_38 (= ?v_72 ?v_73)))) (let ((?v_75 (ite ?v_74 ?v_39 BOOOB_46_init_rob_head))) (let ((?v_113 (or (and (not ?v_74) (not (and ?v_37 (= ?v_46 ?v_73)))) (and (and ?v_43 (= ?v_48 ?v_75)) (and ?v_37 (= ?v_75 BOOOB_46_init_rob_head))))) (?v_79 (or (and ?v_60 ?v_67) ?v_77)) (?v_81 (and (and ?v_43 (= ?v_48 ?v_53)) ?v_62)) (?v_84 (or ?v_60 (and (not (and (and ?v_69 ?v_80) ?v_70)) ?v_62)))) (let ((?v_85 (or (and (and ?v_58 (= ?v_63 ?v_53)) (and (and (and ?v_71 ?v_79) (not ?v_81)) ?v_84)) ?v_81))) (let ((?v_240 (and ?v_233 (or (and (and ?v_102 (= ?v_108 ?v_53)) (and (and (and (or (and ?v_57 ?v_103) (and ?v_76 (or (and ?v_58 (and (and (not ?v_71) ?v_65) ?v_78)) ?v_71))) (or (and ?v_57 ?v_113) (and ?v_76 (or (and ?v_58 (and (and (not ?v_79) ?v_65) ?v_78)) ?v_79)))) (not ?v_85)) (or ?v_57 (and (not (and (and ?v_82 ?v_80) ?v_83)) ?v_84)))) ?v_85))) (?v_148 (ite ?v_86 (+ 1 ?v_87) ?v_87))) (let ((?v_234 (not (= ?v_53 ?v_148)))) (let ((?v_88 (ite (and ?v_240 ?v_234) (+ 1 ?v_53) ?v_53))) (let ((?v_101 (and ?v_86 (= ?v_88 ?v_87))) (?v_121 (BOOOB_46_Decode_dest ?v_15)) (?v_91 (BOOOB_46_Decode_src1 ?v_16))) (let ((?v_93 (and ?v_51 (= ?v_121 ?v_91))) (?v_122 (ite (and ?v_38 ?v_90) ?v_72 (ite ?v_37 ?v_46 BOOOB_46_init_null_reg))) (?v_92 (and ?v_38 (= ?v_72 ?v_91)))) (let ((?v_94 (ite ?v_92 ?v_39 BOOOB_46_init_rob_head))) (let ((?v_95 (ite ?v_93 ?v_52 ?v_94))) (let ((?v_96 (and ?v_38 (= ?v_95 ?v_39))) (?v_99 (= ?v_95 BOOOB_46_init_rob_head))) (let ((?v_97 (and ?v_37 ?v_99))) (let ((?v_98 (and (not ?v_96) (or (and ?v_43 (and (and (not ?v_97) ?v_44) ?v_61)) ?v_97))) (?v_100 (and (and ?v_43 (= ?v_48 ?v_95)) ?v_97))) (let ((?v_171 (or (and (not ?v_93) (or (and (and ?v_89 (= ?v_122 ?v_91)) (= ?v_94 BOOOB_46_init_rob_head)) (and (not ?v_92) (not (and ?v_37 (= ?v_46 ?v_91)))))) (or (and (and ?v_58 (= ?v_63 ?v_95)) (and (and (and (or (and ?v_96 ?v_59) ?v_98) (or (and ?v_96 ?v_67) ?v_98)) (not ?v_100)) (or ?v_96 (and (not (and (and ?v_69 ?v_99) ?v_70)) ?v_97)))) ?v_100))) (?v_133 (not ?v_101)) (?v_104 (and ?v_51 (= ?v_88 ?v_52)))) (let ((?v_134 (not ?v_104)) (?v_105 (and ?v_38 (= ?v_88 ?v_39))) (?v_139 (= ?v_88 BOOOB_46_init_rob_head))) (let ((?v_106 (and ?v_37 ?v_139))) (let ((?v_135 (and (not ?v_105) (or (and ?v_43 (and (and (not ?v_106) ?v_44) ?v_61)) ?v_106)))) (let ((?v_107 (or (and ?v_105 ?v_59) ?v_135))) (let ((?v_120 (or (and ?v_104 ?v_103) (and ?v_134 (or (and ?v_58 (and (and (not ?v_107) ?v_65) ?v_78)) ?v_107)))) (?v_109 (and ?v_51 (= ?v_108 ?v_52)))) (let ((?v_114 (not ?v_109)) (?v_110 (and ?v_38 (= ?v_108 ?v_39))) (?v_117 (= ?v_108 BOOOB_46_init_rob_head))) (let ((?v_111 (and ?v_37 ?v_117))) (let ((?v_115 (and (not ?v_110) (or (and ?v_43 (and (and (not ?v_111) ?v_44) ?v_61)) ?v_111)))) (let ((?v_112 (or (and ?v_110 ?v_59) ?v_115)) (?v_116 (or (and ?v_110 ?v_67) ?v_115)) (?v_118 (and (and ?v_43 (= ?v_48 ?v_108)) ?v_111)) (?v_119 (or ?v_110 (and (not (and (and ?v_69 ?v_117) ?v_70)) ?v_111)))) (let ((?v_137 (and (and (and (or (and ?v_109 ?v_103) (and ?v_114 (or (and ?v_58 (and (and (not ?v_112) ?v_65) ?v_78)) ?v_112))) (or (and ?v_109 ?v_113) (and ?v_114 (or (and ?v_58 (and (and (not ?v_116) ?v_65) ?v_78)) ?v_116)))) (not (or (and (and ?v_58 (= ?v_63 ?v_108)) (and (and (and ?v_112 ?v_116) (not ?v_118)) ?v_119)) ?v_118))) (or ?v_109 (and (not (and (and ?v_82 ?v_117) ?v_83)) ?v_119)))) (?v_123 (BOOOB_46_Decode_src2 ?v_16))) (let ((?v_125 (and ?v_51 (= ?v_121 ?v_123))) (?v_124 (and ?v_38 (= ?v_72 ?v_123)))) (let ((?v_126 (ite ?v_124 ?v_39 BOOOB_46_init_rob_head))) (let ((?v_127 (ite ?v_125 ?v_52 ?v_126))) (let ((?v_128 (and ?v_38 (= ?v_127 ?v_39))) (?v_131 (= ?v_127 BOOOB_46_init_rob_head))) (let ((?v_129 (and ?v_37 ?v_131))) (let ((?v_130 (and (not ?v_128) (or (and ?v_43 (and (and (not ?v_129) ?v_44) ?v_61)) ?v_129))) (?v_132 (and (and ?v_43 (= ?v_48 ?v_127)) ?v_129))) (let ((?v_186 (or (and (not ?v_125) (or (and (and ?v_89 (= ?v_122 ?v_123)) (= ?v_126 BOOOB_46_init_rob_head)) (and (not ?v_124) (not (and ?v_37 (= ?v_46 ?v_123)))))) (or (and (and ?v_58 (= ?v_63 ?v_127)) (and (and (and (or (and ?v_128 ?v_59) ?v_130) (or (and ?v_128 ?v_67) ?v_130)) (not ?v_132)) (or ?v_128 (and (not (and (and ?v_69 ?v_131) ?v_70)) ?v_129)))) ?v_132))) (?v_136 (or (and ?v_105 ?v_67) ?v_135))) (let ((?v_138 (or (and ?v_104 ?v_113) (and ?v_134 (or (and ?v_58 (and (and (not ?v_136) ?v_65) ?v_78)) ?v_136)))) (?v_140 (and (and ?v_43 (= ?v_48 ?v_88)) ?v_106)) (?v_141 (or ?v_105 (and (not (and (and ?v_69 ?v_139) ?v_70)) ?v_106)))) (let ((?v_142 (or (and (and ?v_58 (= ?v_63 ?v_88)) (and (and (and ?v_107 ?v_136) (not ?v_140)) ?v_141)) ?v_140)) (?v_145 (or ?v_104 (and (not (and (and ?v_82 ?v_139) ?v_83)) ?v_141)))) (let ((?v_146 (or (and (and ?v_102 (= ?v_108 ?v_88)) (and (and (and ?v_120 ?v_138) (not ?v_142)) ?v_145)) ?v_142))) (let ((?v_362 (and ?v_355 (or (and (and ?v_170 (= ?v_179 ?v_88)) (and (and (and (or (and ?v_101 ?v_171) (and ?v_133 (or (and ?v_102 (and (and (not ?v_120) (= (ite ?v_104 ?v_56 BOOOB_46_init_rob_head) ?v_108)) ?v_137)) ?v_120))) (or (and ?v_101 ?v_186) (and ?v_133 (or (and ?v_102 (and (and (not ?v_138) (= (ite ?v_104 ?v_75 BOOOB_46_init_rob_head) ?v_108)) ?v_137)) ?v_138)))) (not ?v_146)) (or ?v_101 (and (not (and (and ?v_143 (= ?v_88 ?v_41)) ?v_144)) ?v_145)))) ?v_146))) (?v_238 (ite ?v_147 (+ 1 ?v_148) ?v_148))) (let ((?v_356 (not (= ?v_88 ?v_238)))) (let ((?v_149 (ite (and ?v_362 ?v_356) (+ 1 ?v_88) ?v_88))) (let ((?v_169 (and ?v_147 (= ?v_149 ?v_148))) (?v_198 (BOOOB_46_Decode_dest ?v_16)) (?v_151 (BOOOB_46_Decode_src1 ?v_17))) (let ((?v_155 (and ?v_86 (= ?v_198 ?v_151))) (?v_199 (ite (and ?v_51 (= ?v_41 ?v_52)) ?v_121 (ite ?v_42 ?v_72 (ite ?v_45 ?v_46 BOOOB_46_init_null_reg)))) (?v_152 (and ?v_51 (= ?v_121 ?v_151))) (?v_154 (and ?v_38 (= ?v_72 ?v_151)))) (let ((?v_153 (ite ?v_154 ?v_39 BOOOB_46_init_rob_head))) (let ((?v_156 (ite ?v_152 ?v_52 ?v_153))) (let ((?v_157 (ite ?v_155 ?v_87 ?v_156))) (let ((?v_158 (and ?v_51 (= ?v_157 ?v_52)))) (let ((?v_162 (not ?v_158)) (?v_159 (and ?v_38 (= ?v_157 ?v_39))) (?v_165 (= ?v_157 BOOOB_46_init_rob_head))) (let ((?v_160 (and ?v_37 ?v_165))) (let ((?v_163 (and (not ?v_159) (or (and ?v_43 (and (and (not ?v_160) ?v_44) ?v_61)) ?v_160)))) (let ((?v_161 (or (and ?v_159 ?v_59) ?v_163)) (?v_164 (or (and ?v_159 ?v_67) ?v_163)) (?v_166 (and (and ?v_43 (= ?v_48 ?v_157)) ?v_160)) (?v_167 (or ?v_159 (and (not (and (and ?v_69 ?v_165) ?v_70)) ?v_160)))) (let ((?v_168 (or (and (and ?v_58 (= ?v_63 ?v_157)) (and (and (and ?v_161 ?v_164) (not ?v_166)) ?v_167)) ?v_166))) (let ((?v_269 (or (and (not ?v_155) (or (and (and ?v_150 (= ?v_199 ?v_151)) (= ?v_156 ?v_41)) (and (not ?v_152) (or (and (and ?v_89 (= ?v_122 ?v_151)) (= ?v_153 BOOOB_46_init_rob_head)) (and (not ?v_154) (not (and ?v_37 (= ?v_46 ?v_151)))))))) (or (and (and ?v_102 (= ?v_108 ?v_157)) (and (and (and (or (and ?v_158 ?v_103) (and ?v_162 (or (and ?v_58 (and (and (not ?v_161) ?v_65) ?v_78)) ?v_161))) (or (and ?v_158 ?v_113) (and ?v_162 (or (and ?v_58 (and (and (not ?v_164) ?v_65) ?v_78)) ?v_164)))) (not ?v_168)) (or ?v_158 (and (not (and (and ?v_82 ?v_165) ?v_83)) ?v_167)))) ?v_168))) (?v_218 (not ?v_169)) (?v_172 (and ?v_86 (= ?v_149 ?v_87)))) (let ((?v_219 (not ?v_172)) (?v_173 (and ?v_51 (= ?v_149 ?v_52)))) (let ((?v_220 (not ?v_173)) (?v_174 (and ?v_38 (= ?v_149 ?v_39))) (?v_227 (= ?v_149 BOOOB_46_init_rob_head))) (let ((?v_175 (and ?v_37 ?v_227))) (let ((?v_221 (and (not ?v_174) (or (and ?v_43 (and (and (not ?v_175) ?v_44) ?v_61)) ?v_175)))) (let ((?v_176 (or (and ?v_174 ?v_59) ?v_221))) (let ((?v_177 (or (and ?v_173 ?v_103) (and ?v_220 (or (and ?v_58 (and (and (not ?v_176) ?v_65) ?v_78)) ?v_176)))) (?v_178 (ite ?v_173 ?v_56 BOOOB_46_init_rob_head))) (let ((?v_197 (or (and ?v_172 ?v_171) (and ?v_219 (or (and ?v_102 (and (and (not ?v_177) (= ?v_178 ?v_108)) ?v_137)) ?v_177)))) (?v_180 (and ?v_86 (= ?v_179 ?v_87)))) (let ((?v_187 (not ?v_180)) (?v_181 (and ?v_51 (= ?v_179 ?v_52)))) (let ((?v_188 (not ?v_181)) (?v_182 (and ?v_38 (= ?v_179 ?v_39))) (?v_192 (= ?v_179 BOOOB_46_init_rob_head))) (let ((?v_183 (and ?v_37 ?v_192))) (let ((?v_189 (and (not ?v_182) (or (and ?v_43 (and (and (not ?v_183) ?v_44) ?v_61)) ?v_183)))) (let ((?v_184 (or (and ?v_182 ?v_59) ?v_189))) (let ((?v_185 (or (and ?v_181 ?v_103) (and ?v_188 (or (and ?v_58 (and (and (not ?v_184) ?v_65) ?v_78)) ?v_184)))) (?v_190 (or (and ?v_182 ?v_67) ?v_189))) (let ((?v_191 (or (and ?v_181 ?v_113) (and ?v_188 (or (and ?v_58 (and (and (not ?v_190) ?v_65) ?v_78)) ?v_190)))) (?v_193 (and (and ?v_43 (= ?v_48 ?v_179)) ?v_183)) (?v_194 (or ?v_182 (and (not (and (and ?v_69 ?v_192) ?v_70)) ?v_183)))) (let ((?v_195 (or (and (and ?v_58 (= ?v_63 ?v_179)) (and (and (and ?v_184 ?v_190) (not ?v_193)) ?v_194)) ?v_193)) (?v_196 (or ?v_181 (and (not (and (and ?v_82 ?v_192) ?v_83)) ?v_194)))) (let ((?v_225 (and (and (and (or (and ?v_180 ?v_171) (and ?v_187 (or (and ?v_102 (and (and (not ?v_185) (= (ite ?v_181 ?v_56 BOOOB_46_init_rob_head) ?v_108)) ?v_137)) ?v_185))) (or (and ?v_180 ?v_186) (and ?v_187 (or (and ?v_102 (and (and (not ?v_191) (= (ite ?v_181 ?v_75 BOOOB_46_init_rob_head) ?v_108)) ?v_137)) ?v_191)))) (not (or (and (and ?v_102 (= ?v_108 ?v_179)) (and (and (and ?v_185 ?v_191) (not ?v_195)) ?v_196)) ?v_195))) (or ?v_180 (and (not (and (and ?v_143 (= ?v_179 ?v_41)) ?v_144)) ?v_196)))) (?v_200 (BOOOB_46_Decode_src2 ?v_17))) (let ((?v_204 (and ?v_86 (= ?v_198 ?v_200))) (?v_201 (and ?v_51 (= ?v_121 ?v_200))) (?v_203 (and ?v_38 (= ?v_72 ?v_200)))) (let ((?v_202 (ite ?v_203 ?v_39 BOOOB_46_init_rob_head))) (let ((?v_205 (ite ?v_201 ?v_52 ?v_202))) (let ((?v_206 (ite ?v_204 ?v_87 ?v_205))) (let ((?v_207 (and ?v_51 (= ?v_206 ?v_52)))) (let ((?v_211 (not ?v_207)) (?v_208 (and ?v_38 (= ?v_206 ?v_39))) (?v_214 (= ?v_206 BOOOB_46_init_rob_head))) (let ((?v_209 (and ?v_37 ?v_214))) (let ((?v_212 (and (not ?v_208) (or (and ?v_43 (and (and (not ?v_209) ?v_44) ?v_61)) ?v_209)))) (let ((?v_210 (or (and ?v_208 ?v_59) ?v_212)) (?v_213 (or (and ?v_208 ?v_67) ?v_212)) (?v_215 (and (and ?v_43 (= ?v_48 ?v_206)) ?v_209)) (?v_216 (or ?v_208 (and (not (and (and ?v_69 ?v_214) ?v_70)) ?v_209)))) (let ((?v_217 (or (and (and ?v_58 (= ?v_63 ?v_206)) (and (and (and ?v_210 ?v_213) (not ?v_215)) ?v_216)) ?v_215))) (let ((?v_290 (or (and (not ?v_204) (or (and (and ?v_150 (= ?v_199 ?v_200)) (= ?v_205 ?v_41)) (and (not ?v_201) (or (and (and ?v_89 (= ?v_122 ?v_200)) (= ?v_202 BOOOB_46_init_rob_head)) (and (not ?v_203) (not (and ?v_37 (= ?v_46 ?v_200)))))))) (or (and (and ?v_102 (= ?v_108 ?v_206)) (and (and (and (or (and ?v_207 ?v_103) (and ?v_211 (or (and ?v_58 (and (and (not ?v_210) ?v_65) ?v_78)) ?v_210))) (or (and ?v_207 ?v_113) (and ?v_211 (or (and ?v_58 (and (and (not ?v_213) ?v_65) ?v_78)) ?v_213)))) (not ?v_217)) (or ?v_207 (and (not (and (and ?v_82 ?v_214) ?v_83)) ?v_216)))) ?v_217))) (?v_222 (or (and ?v_174 ?v_67) ?v_221))) (let ((?v_223 (or (and ?v_173 ?v_113) (and ?v_220 (or (and ?v_58 (and (and (not ?v_222) ?v_65) ?v_78)) ?v_222)))) (?v_224 (ite ?v_173 ?v_75 BOOOB_46_init_rob_head))) (let ((?v_226 (or (and ?v_172 ?v_186) (and ?v_219 (or (and ?v_102 (and (and (not ?v_223) (= ?v_224 ?v_108)) ?v_137)) ?v_223)))) (?v_228 (and (and ?v_43 (= ?v_48 ?v_149)) ?v_175)) (?v_229 (or ?v_174 (and (not (and (and ?v_69 ?v_227) ?v_70)) ?v_175)))) (let ((?v_230 (or (and (and ?v_58 (= ?v_63 ?v_149)) (and (and (and ?v_176 ?v_222) (not ?v_228)) ?v_229)) ?v_228)) (?v_231 (or ?v_173 (and (not (and (and ?v_82 ?v_227) ?v_83)) ?v_229)))) (let ((?v_232 (or (and (and ?v_102 (= ?v_108 ?v_149)) (and (and (and ?v_177 ?v_223) (not ?v_230)) ?v_231)) ?v_230)) (?v_235 (or ?v_172 (and (not (and (and ?v_143 (= ?v_149 ?v_41)) ?v_144)) ?v_231)))) (let ((?v_236 (or (and (and ?v_170 (= ?v_179 ?v_149)) (and (and (and ?v_197 ?v_226) (not ?v_232)) ?v_235)) ?v_232))) (let ((?v_525 (and ?v_513 (or (and (and ?v_268 (= ?v_280 ?v_149)) (and (and (and (or (and ?v_169 ?v_269) (and ?v_218 (or (and ?v_170 (and (and (not ?v_197) (= (ite ?v_172 ?v_95 ?v_178) ?v_179)) ?v_225)) ?v_197))) (or (and ?v_169 ?v_290) (and ?v_218 (or (and ?v_170 (and (and (not ?v_226) (= (ite ?v_172 ?v_127 ?v_224) ?v_179)) ?v_225)) ?v_226)))) (not ?v_236)) (or ?v_169 (and (not (and (and ?v_233 (= ?v_149 ?v_53)) ?v_234)) ?v_235)))) ?v_236))) (?v_360 (ite ?v_237 (+ 1 ?v_238) ?v_238))) (let ((?v_514 (not (= ?v_149 ?v_360)))) (let ((?v_239 (ite (and ?v_525 ?v_514) (+ 1 ?v_149) ?v_149))) (let ((?v_267 (and ?v_237 (= ?v_239 ?v_238))) (?v_307 (BOOOB_46_Decode_dest ?v_17)) (?v_241 (BOOOB_46_Decode_src1 ?v_18))) (let ((?v_247 (and ?v_147 (= ?v_307 ?v_241))) (?v_308 (ite (and ?v_86 (= ?v_53 ?v_87)) ?v_198 (ite ?v_57 ?v_121 (ite ?v_60 ?v_72 (ite ?v_62 ?v_46 BOOOB_46_init_null_reg))))) (?v_242 (and ?v_86 (= ?v_198 ?v_241))) (?v_244 (and ?v_51 (= ?v_121 ?v_241))) (?v_246 (and ?v_38 (= ?v_72 ?v_241)))) (let ((?v_245 (ite ?v_246 ?v_39 BOOOB_46_init_rob_head))) (let ((?v_243 (ite ?v_244 ?v_52 ?v_245))) (let ((?v_248 (ite ?v_242 ?v_87 ?v_243))) (let ((?v_249 (ite ?v_247 ?v_148 ?v_248))) (let ((?v_250 (and ?v_86 (= ?v_249 ?v_87)))) (let ((?v_256 (not ?v_250)) (?v_251 (and ?v_51 (= ?v_249 ?v_52)))) (let ((?v_257 (not ?v_251)) (?v_252 (and ?v_38 (= ?v_249 ?v_39))) (?v_261 (= ?v_249 BOOOB_46_init_rob_head))) (let ((?v_253 (and ?v_37 ?v_261))) (let ((?v_258 (and (not ?v_252) (or (and ?v_43 (and (and (not ?v_253) ?v_44) ?v_61)) ?v_253)))) (let ((?v_254 (or (and ?v_252 ?v_59) ?v_258))) (let ((?v_255 (or (and ?v_251 ?v_103) (and ?v_257 (or (and ?v_58 (and (and (not ?v_254) ?v_65) ?v_78)) ?v_254)))) (?v_259 (or (and ?v_252 ?v_67) ?v_258))) (let ((?v_260 (or (and ?v_251 ?v_113) (and ?v_257 (or (and ?v_58 (and (and (not ?v_259) ?v_65) ?v_78)) ?v_259)))) (?v_262 (and (and ?v_43 (= ?v_48 ?v_249)) ?v_253)) (?v_263 (or ?v_252 (and (not (and (and ?v_69 ?v_261) ?v_70)) ?v_253)))) (let ((?v_264 (or (and (and ?v_58 (= ?v_63 ?v_249)) (and (and (and ?v_254 ?v_259) (not ?v_262)) ?v_263)) ?v_262)) (?v_265 (or ?v_251 (and (not (and (and ?v_82 ?v_261) ?v_83)) ?v_263)))) (let ((?v_266 (or (and (and ?v_102 (= ?v_108 ?v_249)) (and (and (and ?v_255 ?v_260) (not ?v_264)) ?v_265)) ?v_264))) (let ((?v_401 (or (and (not ?v_247) (or (and (and ?v_240 (= ?v_308 ?v_241)) (= ?v_248 ?v_53)) (and (not ?v_242) (or (and (and ?v_150 (= ?v_199 ?v_241)) (= ?v_243 ?v_41)) (and (not ?v_244) (or (and (and ?v_89 (= ?v_122 ?v_241)) (= ?v_245 BOOOB_46_init_rob_head)) (and (not ?v_246) (not (and ?v_37 (= ?v_46 ?v_241)))))))))) (or (and (and ?v_170 (= ?v_179 ?v_249)) (and (and (and (or (and ?v_250 ?v_171) (and ?v_256 (or (and ?v_102 (and (and (not ?v_255) (= (ite ?v_251 ?v_56 BOOOB_46_init_rob_head) ?v_108)) ?v_137)) ?v_255))) (or (and ?v_250 ?v_186) (and ?v_256 (or (and ?v_102 (and (and (not ?v_260) (= (ite ?v_251 ?v_75 BOOOB_46_init_rob_head) ?v_108)) ?v_137)) ?v_260)))) (not ?v_266)) (or ?v_250 (and (not (and (and ?v_143 (= ?v_249 ?v_41)) ?v_144)) ?v_265)))) ?v_266))) (?v_335 (not ?v_267)) (?v_270 (and ?v_147 (= ?v_239 ?v_148)))) (let ((?v_336 (not ?v_270)) (?v_271 (and ?v_86 (= ?v_239 ?v_87)))) (let ((?v_337 (not ?v_271)) (?v_272 (and ?v_51 (= ?v_239 ?v_52)))) (let ((?v_338 (not ?v_272)) (?v_273 (and ?v_38 (= ?v_239 ?v_39))) (?v_347 (= ?v_239 BOOOB_46_init_rob_head))) (let ((?v_274 (and ?v_37 ?v_347))) (let ((?v_339 (and (not ?v_273) (or (and ?v_43 (and (and (not ?v_274) ?v_44) ?v_61)) ?v_274)))) (let ((?v_275 (or (and ?v_273 ?v_59) ?v_339))) (let ((?v_276 (or (and ?v_272 ?v_103) (and ?v_338 (or (and ?v_58 (and (and (not ?v_275) ?v_65) ?v_78)) ?v_275)))) (?v_277 (ite ?v_272 ?v_56 BOOOB_46_init_rob_head))) (let ((?v_278 (or (and ?v_271 ?v_171) (and ?v_337 (or (and ?v_102 (and (and (not ?v_276) (= ?v_277 ?v_108)) ?v_137)) ?v_276)))) (?v_279 (ite ?v_271 ?v_95 ?v_277))) (let ((?v_306 (or (and ?v_270 ?v_269) (and ?v_336 (or (and ?v_170 (and (and (not ?v_278) (= ?v_279 ?v_179)) ?v_225)) ?v_278)))) (?v_281 (and ?v_147 (= ?v_280 ?v_148)))) (let ((?v_291 (not ?v_281)) (?v_282 (and ?v_86 (= ?v_280 ?v_87)))) (let ((?v_292 (not ?v_282)) (?v_283 (and ?v_51 (= ?v_280 ?v_52)))) (let ((?v_293 (not ?v_283)) (?v_284 (and ?v_38 (= ?v_280 ?v_39))) (?v_299 (= ?v_280 BOOOB_46_init_rob_head))) (let ((?v_285 (and ?v_37 ?v_299))) (let ((?v_294 (and (not ?v_284) (or (and ?v_43 (and (and (not ?v_285) ?v_44) ?v_61)) ?v_285)))) (let ((?v_286 (or (and ?v_284 ?v_59) ?v_294))) (let ((?v_287 (or (and ?v_283 ?v_103) (and ?v_293 (or (and ?v_58 (and (and (not ?v_286) ?v_65) ?v_78)) ?v_286)))) (?v_288 (ite ?v_283 ?v_56 BOOOB_46_init_rob_head))) (let ((?v_289 (or (and ?v_282 ?v_171) (and ?v_292 (or (and ?v_102 (and (and (not ?v_287) (= ?v_288 ?v_108)) ?v_137)) ?v_287)))) (?v_295 (or (and ?v_284 ?v_67) ?v_294))) (let ((?v_296 (or (and ?v_283 ?v_113) (and ?v_293 (or (and ?v_58 (and (and (not ?v_295) ?v_65) ?v_78)) ?v_295)))) (?v_297 (ite ?v_283 ?v_75 BOOOB_46_init_rob_head))) (let ((?v_298 (or (and ?v_282 ?v_186) (and ?v_292 (or (and ?v_102 (and (and (not ?v_296) (= ?v_297 ?v_108)) ?v_137)) ?v_296)))) (?v_300 (and (and ?v_43 (= ?v_48 ?v_280)) ?v_285)) (?v_301 (or ?v_284 (and (not (and (and ?v_69 ?v_299) ?v_70)) ?v_285)))) (let ((?v_302 (or (and (and ?v_58 (= ?v_63 ?v_280)) (and (and (and ?v_286 ?v_295) (not ?v_300)) ?v_301)) ?v_300)) (?v_303 (or ?v_283 (and (not (and (and ?v_82 ?v_299) ?v_83)) ?v_301)))) (let ((?v_304 (or (and (and ?v_102 (= ?v_108 ?v_280)) (and (and (and ?v_287 ?v_296) (not ?v_302)) ?v_303)) ?v_302)) (?v_305 (or ?v_282 (and (not (and (and ?v_143 (= ?v_280 ?v_41)) ?v_144)) ?v_303)))) (let ((?v_345 (and (and (and (or (and ?v_281 ?v_269) (and ?v_291 (or (and ?v_170 (and (and (not ?v_289) (= (ite ?v_282 ?v_95 ?v_288) ?v_179)) ?v_225)) ?v_289))) (or (and ?v_281 ?v_290) (and ?v_291 (or (and ?v_170 (and (and (not ?v_298) (= (ite ?v_282 ?v_127 ?v_297) ?v_179)) ?v_225)) ?v_298)))) (not (or (and (and ?v_170 (= ?v_179 ?v_280)) (and (and (and ?v_289 ?v_298) (not ?v_304)) ?v_305)) ?v_304))) (or ?v_281 (and (not (and (and ?v_233 (= ?v_280 ?v_53)) ?v_234)) ?v_305)))) (?v_309 (BOOOB_46_Decode_src2 ?v_18))) (let ((?v_315 (and ?v_147 (= ?v_307 ?v_309))) (?v_310 (and ?v_86 (= ?v_198 ?v_309))) (?v_312 (and ?v_51 (= ?v_121 ?v_309))) (?v_314 (and ?v_38 (= ?v_72 ?v_309)))) (let ((?v_313 (ite ?v_314 ?v_39 BOOOB_46_init_rob_head))) (let ((?v_311 (ite ?v_312 ?v_52 ?v_313))) (let ((?v_316 (ite ?v_310 ?v_87 ?v_311))) (let ((?v_317 (ite ?v_315 ?v_148 ?v_316))) (let ((?v_318 (and ?v_86 (= ?v_317 ?v_87)))) (let ((?v_324 (not ?v_318)) (?v_319 (and ?v_51 (= ?v_317 ?v_52)))) (let ((?v_325 (not ?v_319)) (?v_320 (and ?v_38 (= ?v_317 ?v_39))) (?v_329 (= ?v_317 BOOOB_46_init_rob_head))) (let ((?v_321 (and ?v_37 ?v_329))) (let ((?v_326 (and (not ?v_320) (or (and ?v_43 (and (and (not ?v_321) ?v_44) ?v_61)) ?v_321)))) (let ((?v_322 (or (and ?v_320 ?v_59) ?v_326))) (let ((?v_323 (or (and ?v_319 ?v_103) (and ?v_325 (or (and ?v_58 (and (and (not ?v_322) ?v_65) ?v_78)) ?v_322)))) (?v_327 (or (and ?v_320 ?v_67) ?v_326))) (let ((?v_328 (or (and ?v_319 ?v_113) (and ?v_325 (or (and ?v_58 (and (and (not ?v_327) ?v_65) ?v_78)) ?v_327)))) (?v_330 (and (and ?v_43 (= ?v_48 ?v_317)) ?v_321)) (?v_331 (or ?v_320 (and (not (and (and ?v_69 ?v_329) ?v_70)) ?v_321)))) (let ((?v_332 (or (and (and ?v_58 (= ?v_63 ?v_317)) (and (and (and ?v_322 ?v_327) (not ?v_330)) ?v_331)) ?v_330)) (?v_333 (or ?v_319 (and (not (and (and ?v_82 ?v_329) ?v_83)) ?v_331)))) (let ((?v_334 (or (and (and ?v_102 (= ?v_108 ?v_317)) (and (and (and ?v_323 ?v_328) (not ?v_332)) ?v_333)) ?v_332))) (let ((?v_428 (or (and (not ?v_315) (or (and (and ?v_240 (= ?v_308 ?v_309)) (= ?v_316 ?v_53)) (and (not ?v_310) (or (and (and ?v_150 (= ?v_199 ?v_309)) (= ?v_311 ?v_41)) (and (not ?v_312) (or (and (and ?v_89 (= ?v_122 ?v_309)) (= ?v_313 BOOOB_46_init_rob_head)) (and (not ?v_314) (not (and ?v_37 (= ?v_46 ?v_309)))))))))) (or (and (and ?v_170 (= ?v_179 ?v_317)) (and (and (and (or (and ?v_318 ?v_171) (and ?v_324 (or (and ?v_102 (and (and (not ?v_323) (= (ite ?v_319 ?v_56 BOOOB_46_init_rob_head) ?v_108)) ?v_137)) ?v_323))) (or (and ?v_318 ?v_186) (and ?v_324 (or (and ?v_102 (and (and (not ?v_328) (= (ite ?v_319 ?v_75 BOOOB_46_init_rob_head) ?v_108)) ?v_137)) ?v_328)))) (not ?v_334)) (or ?v_318 (and (not (and (and ?v_143 (= ?v_317 ?v_41)) ?v_144)) ?v_333)))) ?v_334))) (?v_340 (or (and ?v_273 ?v_67) ?v_339))) (let ((?v_341 (or (and ?v_272 ?v_113) (and ?v_338 (or (and ?v_58 (and (and (not ?v_340) ?v_65) ?v_78)) ?v_340)))) (?v_342 (ite ?v_272 ?v_75 BOOOB_46_init_rob_head))) (let ((?v_343 (or (and ?v_271 ?v_186) (and ?v_337 (or (and ?v_102 (and (and (not ?v_341) (= ?v_342 ?v_108)) ?v_137)) ?v_341)))) (?v_344 (ite ?v_271 ?v_127 ?v_342))) (let ((?v_346 (or (and ?v_270 ?v_290) (and ?v_336 (or (and ?v_170 (and (and (not ?v_343) (= ?v_344 ?v_179)) ?v_225)) ?v_343)))) (?v_348 (and (and ?v_43 (= ?v_48 ?v_239)) ?v_274)) (?v_349 (or ?v_273 (and (not (and (and ?v_69 ?v_347) ?v_70)) ?v_274)))) (let ((?v_350 (or (and (and ?v_58 (= ?v_63 ?v_239)) (and (and (and ?v_275 ?v_340) (not ?v_348)) ?v_349)) ?v_348)) (?v_351 (or ?v_272 (and (not (and (and ?v_82 ?v_347) ?v_83)) ?v_349)))) (let ((?v_352 (or (and (and ?v_102 (= ?v_108 ?v_239)) (and (and (and ?v_276 ?v_341) (not ?v_350)) ?v_351)) ?v_350)) (?v_353 (or ?v_271 (and (not (and (and ?v_143 (= ?v_239 ?v_41)) ?v_144)) ?v_351)))) (let ((?v_354 (or (and (and ?v_170 (= ?v_179 ?v_239)) (and (and (and ?v_278 ?v_343) (not ?v_352)) ?v_353)) ?v_352)) (?v_357 (or ?v_270 (and (not (and (and ?v_233 (= ?v_239 ?v_53)) ?v_234)) ?v_353)))) (let ((?v_358 (or (and (and ?v_268 (= ?v_280 ?v_239)) (and (and (and ?v_306 ?v_346) (not ?v_354)) ?v_357)) ?v_354))) (let ((?v_522 (and (and ?v_23 ?v_24) (or (and (and ?v_400 (= ?v_415 ?v_239)) (and (and (and (or (and ?v_267 ?v_401) (and ?v_335 (or (and ?v_268 (and (and (not ?v_306) (= (ite ?v_270 ?v_157 ?v_279) ?v_280)) ?v_345)) ?v_306))) (or (and ?v_267 ?v_428) (and ?v_335 (or (and ?v_268 (and (and (not ?v_346) (= (ite ?v_270 ?v_206 ?v_344) ?v_280)) ?v_345)) ?v_346)))) (not ?v_358)) (or ?v_267 (and (not (and (and ?v_355 (= ?v_239 ?v_88)) ?v_356)) ?v_357)))) ?v_358))) (?v_518 (ite ?v_359 (+ 1 ?v_360) ?v_360))) (let ((?v_361 (ite (and ?v_522 (not (= ?v_239 ?v_518))) (+ 1 ?v_239) ?v_239))) (let ((?v_399 (and ?v_359 (= ?v_361 ?v_360))) (?v_450 (BOOOB_46_Decode_dest ?v_18)) (?v_363 (BOOOB_46_Decode_src1 ?v_19))) (let ((?v_371 (and ?v_237 (= ?v_450 ?v_363))) (?v_451 (ite (and ?v_147 (= ?v_88 ?v_148)) ?v_307 (ite ?v_101 ?v_198 (ite ?v_104 ?v_121 (ite ?v_105 ?v_72 (ite ?v_106 ?v_46 BOOOB_46_init_null_reg)))))) (?v_364 (and ?v_147 (= ?v_307 ?v_363))) (?v_366 (and ?v_86 (= ?v_198 ?v_363))) (?v_368 (and ?v_51 (= ?v_121 ?v_363))) (?v_370 (and ?v_38 (= ?v_72 ?v_363)))) (let ((?v_369 (ite ?v_370 ?v_39 BOOOB_46_init_rob_head))) (let ((?v_367 (ite ?v_368 ?v_52 ?v_369))) (let ((?v_365 (ite ?v_366 ?v_87 ?v_367))) (let ((?v_372 (ite ?v_364 ?v_148 ?v_365))) (let ((?v_373 (ite ?v_371 ?v_238 ?v_372))) (let ((?v_374 (and ?v_147 (= ?v_373 ?v_148)))) (let ((?v_383 (not ?v_374)) (?v_375 (and ?v_86 (= ?v_373 ?v_87)))) (let ((?v_384 (not ?v_375)) (?v_376 (and ?v_51 (= ?v_373 ?v_52)))) (let ((?v_385 (not ?v_376)) (?v_377 (and ?v_38 (= ?v_373 ?v_39))) (?v_391 (= ?v_373 BOOOB_46_init_rob_head))) (let ((?v_378 (and ?v_37 ?v_391))) (let ((?v_386 (and (not ?v_377) (or (and ?v_43 (and (and (not ?v_378) ?v_44) ?v_61)) ?v_378)))) (let ((?v_379 (or (and ?v_377 ?v_59) ?v_386))) (let ((?v_380 (or (and ?v_376 ?v_103) (and ?v_385 (or (and ?v_58 (and (and (not ?v_379) ?v_65) ?v_78)) ?v_379)))) (?v_381 (ite ?v_376 ?v_56 BOOOB_46_init_rob_head))) (let ((?v_382 (or (and ?v_375 ?v_171) (and ?v_384 (or (and ?v_102 (and (and (not ?v_380) (= ?v_381 ?v_108)) ?v_137)) ?v_380)))) (?v_387 (or (and ?v_377 ?v_67) ?v_386))) (let ((?v_388 (or (and ?v_376 ?v_113) (and ?v_385 (or (and ?v_58 (and (and (not ?v_387) ?v_65) ?v_78)) ?v_387)))) (?v_389 (ite ?v_376 ?v_75 BOOOB_46_init_rob_head))) (let ((?v_390 (or (and ?v_375 ?v_186) (and ?v_384 (or (and ?v_102 (and (and (not ?v_388) (= ?v_389 ?v_108)) ?v_137)) ?v_388)))) (?v_392 (and (and ?v_43 (= ?v_48 ?v_373)) ?v_378)) (?v_393 (or ?v_377 (and (not (and (and ?v_69 ?v_391) ?v_70)) ?v_378)))) (let ((?v_394 (or (and (and ?v_58 (= ?v_63 ?v_373)) (and (and (and ?v_379 ?v_387) (not ?v_392)) ?v_393)) ?v_392)) (?v_395 (or ?v_376 (and (not (and (and ?v_82 ?v_391) ?v_83)) ?v_393)))) (let ((?v_396 (or (and (and ?v_102 (= ?v_108 ?v_373)) (and (and (and ?v_380 ?v_388) (not ?v_394)) ?v_395)) ?v_394)) (?v_397 (or ?v_375 (and (not (and (and ?v_143 (= ?v_373 ?v_41)) ?v_144)) ?v_395)))) (let ((?v_398 (or (and (and ?v_170 (= ?v_179 ?v_373)) (and (and (and ?v_382 ?v_390) (not ?v_396)) ?v_397)) ?v_396)) (?v_488 (not ?v_399)) (?v_402 (and ?v_237 (= ?v_361 ?v_238)))) (let ((?v_489 (not ?v_402)) (?v_403 (and ?v_147 (= ?v_361 ?v_148)))) (let ((?v_490 (not ?v_403)) (?v_404 (and ?v_86 (= ?v_361 ?v_87)))) (let ((?v_491 (not ?v_404)) (?v_405 (and ?v_51 (= ?v_361 ?v_52)))) (let ((?v_492 (not ?v_405)) (?v_406 (and ?v_38 (= ?v_361 ?v_39))) (?v_503 (= ?v_361 BOOOB_46_init_rob_head))) (let ((?v_407 (and ?v_37 ?v_503))) (let ((?v_493 (and (not ?v_406) (or (and ?v_43 (and (and (not ?v_407) ?v_44) ?v_61)) ?v_407)))) (let ((?v_408 (or (and ?v_406 ?v_59) ?v_493))) (let ((?v_409 (or (and ?v_405 ?v_103) (and ?v_492 (or (and ?v_58 (and (and (not ?v_408) ?v_65) ?v_78)) ?v_408)))) (?v_410 (ite ?v_405 ?v_56 BOOOB_46_init_rob_head))) (let ((?v_411 (or (and ?v_404 ?v_171) (and ?v_491 (or (and ?v_102 (and (and (not ?v_409) (= ?v_410 ?v_108)) ?v_137)) ?v_409)))) (?v_412 (ite ?v_404 ?v_95 ?v_410))) (let ((?v_413 (or (and ?v_403 ?v_269) (and ?v_490 (or (and ?v_170 (and (and (not ?v_411) (= ?v_412 ?v_179)) ?v_225)) ?v_411)))) (?v_414 (ite ?v_403 ?v_157 ?v_412))) (let ((?v_449 (or (and ?v_402 ?v_401) (and ?v_489 (or (and ?v_268 (and (and (not ?v_413) (= ?v_414 ?v_280)) ?v_345)) ?v_413)))) (?v_416 (and ?v_237 (= ?v_415 ?v_238)))) (let ((?v_429 (not ?v_416)) (?v_417 (and ?v_147 (= ?v_415 ?v_148)))) (let ((?v_430 (not ?v_417)) (?v_418 (and ?v_86 (= ?v_415 ?v_87)))) (let ((?v_431 (not ?v_418)) (?v_419 (and ?v_51 (= ?v_415 ?v_52)))) (let ((?v_432 (not ?v_419)) (?v_420 (and ?v_38 (= ?v_415 ?v_39))) (?v_440 (= ?v_415 BOOOB_46_init_rob_head))) (let ((?v_421 (and ?v_37 ?v_440))) (let ((?v_433 (and (not ?v_420) (or (and ?v_43 (and (and (not ?v_421) ?v_44) ?v_61)) ?v_421)))) (let ((?v_422 (or (and ?v_420 ?v_59) ?v_433))) (let ((?v_423 (or (and ?v_419 ?v_103) (and ?v_432 (or (and ?v_58 (and (and (not ?v_422) ?v_65) ?v_78)) ?v_422)))) (?v_424 (ite ?v_419 ?v_56 BOOOB_46_init_rob_head))) (let ((?v_425 (or (and ?v_418 ?v_171) (and ?v_431 (or (and ?v_102 (and (and (not ?v_423) (= ?v_424 ?v_108)) ?v_137)) ?v_423)))) (?v_426 (ite ?v_418 ?v_95 ?v_424))) (let ((?v_427 (or (and ?v_417 ?v_269) (and ?v_430 (or (and ?v_170 (and (and (not ?v_425) (= ?v_426 ?v_179)) ?v_225)) ?v_425)))) (?v_434 (or (and ?v_420 ?v_67) ?v_433))) (let ((?v_435 (or (and ?v_419 ?v_113) (and ?v_432 (or (and ?v_58 (and (and (not ?v_434) ?v_65) ?v_78)) ?v_434)))) (?v_436 (ite ?v_419 ?v_75 BOOOB_46_init_rob_head))) (let ((?v_437 (or (and ?v_418 ?v_186) (and ?v_431 (or (and ?v_102 (and (and (not ?v_435) (= ?v_436 ?v_108)) ?v_137)) ?v_435)))) (?v_438 (ite ?v_418 ?v_127 ?v_436))) (let ((?v_439 (or (and ?v_417 ?v_290) (and ?v_430 (or (and ?v_170 (and (and (not ?v_437) (= ?v_438 ?v_179)) ?v_225)) ?v_437)))) (?v_441 (and (and ?v_43 (= ?v_48 ?v_415)) ?v_421)) (?v_442 (or ?v_420 (and (not (and (and ?v_69 ?v_440) ?v_70)) ?v_421)))) (let ((?v_443 (or (and (and ?v_58 (= ?v_63 ?v_415)) (and (and (and ?v_422 ?v_434) (not ?v_441)) ?v_442)) ?v_441)) (?v_444 (or ?v_419 (and (not (and (and ?v_82 ?v_440) ?v_83)) ?v_442)))) (let ((?v_445 (or (and (and ?v_102 (= ?v_108 ?v_415)) (and (and (and ?v_423 ?v_435) (not ?v_443)) ?v_444)) ?v_443)) (?v_446 (or ?v_418 (and (not (and (and ?v_143 (= ?v_415 ?v_41)) ?v_144)) ?v_444)))) (let ((?v_447 (or (and (and ?v_170 (= ?v_179 ?v_415)) (and (and (and ?v_425 ?v_437) (not ?v_445)) ?v_446)) ?v_445)) (?v_448 (or ?v_417 (and (not (and (and ?v_233 (= ?v_415 ?v_53)) ?v_234)) ?v_446)))) (let ((?v_501 (and (and (and (or (and ?v_416 ?v_401) (and ?v_429 (or (and ?v_268 (and (and (not ?v_427) (= (ite ?v_417 ?v_157 ?v_426) ?v_280)) ?v_345)) ?v_427))) (or (and ?v_416 ?v_428) (and ?v_429 (or (and ?v_268 (and (and (not ?v_439) (= (ite ?v_417 ?v_206 ?v_438) ?v_280)) ?v_345)) ?v_439)))) (not (or (and (and ?v_268 (= ?v_280 ?v_415)) (and (and (and ?v_427 ?v_439) (not ?v_447)) ?v_448)) ?v_447))) (or ?v_416 (and (not (and (and ?v_355 (= ?v_415 ?v_88)) ?v_356)) ?v_448)))) (?v_452 (BOOOB_46_Decode_src2 ?v_19))) (let ((?v_460 (and ?v_237 (= ?v_450 ?v_452))) (?v_453 (and ?v_147 (= ?v_307 ?v_452))) (?v_455 (and ?v_86 (= ?v_198 ?v_452))) (?v_457 (and ?v_51 (= ?v_121 ?v_452))) (?v_459 (and ?v_38 (= ?v_72 ?v_452)))) (let ((?v_458 (ite ?v_459 ?v_39 BOOOB_46_init_rob_head))) (let ((?v_456 (ite ?v_457 ?v_52 ?v_458))) (let ((?v_454 (ite ?v_455 ?v_87 ?v_456))) (let ((?v_461 (ite ?v_453 ?v_148 ?v_454))) (let ((?v_462 (ite ?v_460 ?v_238 ?v_461))) (let ((?v_463 (and ?v_147 (= ?v_462 ?v_148)))) (let ((?v_472 (not ?v_463)) (?v_464 (and ?v_86 (= ?v_462 ?v_87)))) (let ((?v_473 (not ?v_464)) (?v_465 (and ?v_51 (= ?v_462 ?v_52)))) (let ((?v_474 (not ?v_465)) (?v_466 (and ?v_38 (= ?v_462 ?v_39))) (?v_480 (= ?v_462 BOOOB_46_init_rob_head))) (let ((?v_467 (and ?v_37 ?v_480))) (let ((?v_475 (and (not ?v_466) (or (and ?v_43 (and (and (not ?v_467) ?v_44) ?v_61)) ?v_467)))) (let ((?v_468 (or (and ?v_466 ?v_59) ?v_475))) (let ((?v_469 (or (and ?v_465 ?v_103) (and ?v_474 (or (and ?v_58 (and (and (not ?v_468) ?v_65) ?v_78)) ?v_468)))) (?v_470 (ite ?v_465 ?v_56 BOOOB_46_init_rob_head))) (let ((?v_471 (or (and ?v_464 ?v_171) (and ?v_473 (or (and ?v_102 (and (and (not ?v_469) (= ?v_470 ?v_108)) ?v_137)) ?v_469)))) (?v_476 (or (and ?v_466 ?v_67) ?v_475))) (let ((?v_477 (or (and ?v_465 ?v_113) (and ?v_474 (or (and ?v_58 (and (and (not ?v_476) ?v_65) ?v_78)) ?v_476)))) (?v_478 (ite ?v_465 ?v_75 BOOOB_46_init_rob_head))) (let ((?v_479 (or (and ?v_464 ?v_186) (and ?v_473 (or (and ?v_102 (and (and (not ?v_477) (= ?v_478 ?v_108)) ?v_137)) ?v_477)))) (?v_481 (and (and ?v_43 (= ?v_48 ?v_462)) ?v_467)) (?v_482 (or ?v_466 (and (not (and (and ?v_69 ?v_480) ?v_70)) ?v_467)))) (let ((?v_483 (or (and (and ?v_58 (= ?v_63 ?v_462)) (and (and (and ?v_468 ?v_476) (not ?v_481)) ?v_482)) ?v_481)) (?v_484 (or ?v_465 (and (not (and (and ?v_82 ?v_480) ?v_83)) ?v_482)))) (let ((?v_485 (or (and (and ?v_102 (= ?v_108 ?v_462)) (and (and (and ?v_469 ?v_477) (not ?v_483)) ?v_484)) ?v_483)) (?v_486 (or ?v_464 (and (not (and (and ?v_143 (= ?v_462 ?v_41)) ?v_144)) ?v_484)))) (let ((?v_487 (or (and (and ?v_170 (= ?v_179 ?v_462)) (and (and (and ?v_471 ?v_479) (not ?v_485)) ?v_486)) ?v_485)) (?v_494 (or (and ?v_406 ?v_67) ?v_493))) (let ((?v_495 (or (and ?v_405 ?v_113) (and ?v_492 (or (and ?v_58 (and (and (not ?v_494) ?v_65) ?v_78)) ?v_494)))) (?v_496 (ite ?v_405 ?v_75 BOOOB_46_init_rob_head))) (let ((?v_497 (or (and ?v_404 ?v_186) (and ?v_491 (or (and ?v_102 (and (and (not ?v_495) (= ?v_496 ?v_108)) ?v_137)) ?v_495)))) (?v_498 (ite ?v_404 ?v_127 ?v_496))) (let ((?v_499 (or (and ?v_403 ?v_290) (and ?v_490 (or (and ?v_170 (and (and (not ?v_497) (= ?v_498 ?v_179)) ?v_225)) ?v_497)))) (?v_500 (ite ?v_403 ?v_206 ?v_498))) (let ((?v_502 (or (and ?v_402 ?v_428) (and ?v_489 (or (and ?v_268 (and (and (not ?v_499) (= ?v_500 ?v_280)) ?v_345)) ?v_499)))) (?v_504 (and (and ?v_43 (= ?v_48 ?v_361)) ?v_407)) (?v_505 (or ?v_406 (and (not (and (and ?v_69 ?v_503) ?v_70)) ?v_407)))) (let ((?v_506 (or (and (and ?v_58 (= ?v_63 ?v_361)) (and (and (and ?v_408 ?v_494) (not ?v_504)) ?v_505)) ?v_504)) (?v_507 (or ?v_405 (and (not (and (and ?v_82 ?v_503) ?v_83)) ?v_505)))) (let ((?v_508 (or (and (and ?v_102 (= ?v_108 ?v_361)) (and (and (and ?v_409 ?v_495) (not ?v_506)) ?v_507)) ?v_506)) (?v_509 (or ?v_404 (and (not (and (and ?v_143 (= ?v_361 ?v_41)) ?v_144)) ?v_507)))) (let ((?v_510 (or (and (and ?v_170 (= ?v_179 ?v_361)) (and (and (and ?v_411 ?v_497) (not ?v_508)) ?v_509)) ?v_508)) (?v_511 (or ?v_403 (and (not (and (and ?v_233 (= ?v_361 ?v_53)) ?v_234)) ?v_509)))) (let ((?v_512 (or (and (and ?v_268 (= ?v_280 ?v_361)) (and (and (and ?v_413 ?v_499) (not ?v_510)) ?v_511)) ?v_510)) (?v_515 (or ?v_402 (and (not (and (and ?v_355 (= ?v_361 ?v_88)) ?v_356)) ?v_511)))) (let ((?v_516 (or (and (and ?v_400 (= ?v_415 ?v_361)) (and (and (and ?v_449 ?v_502) (not ?v_512)) ?v_515)) ?v_512))) (let ((?v_538 (and (and ?v_21 ?v_22) (or (and (and (and ?v_23 (not ?v_24)) (= (BOOOB_46_New_ex_id ?v_1) ?v_361)) (and (and (and (or (and ?v_399 (or (and (not ?v_371) (or (and (and ?v_362 (= ?v_451 ?v_363)) (= ?v_372 ?v_88)) (and (not ?v_364) (or (and (and ?v_240 (= ?v_308 ?v_363)) (= ?v_365 ?v_53)) (and (not ?v_366) (or (and (and ?v_150 (= ?v_199 ?v_363)) (= ?v_367 ?v_41)) (and (not ?v_368) (or (and (and ?v_89 (= ?v_122 ?v_363)) (= ?v_369 BOOOB_46_init_rob_head)) (and (not ?v_370) (not (and ?v_37 (= ?v_46 ?v_363)))))))))))) (or (and (and ?v_268 (= ?v_280 ?v_373)) (and (and (and (or (and ?v_374 ?v_269) (and ?v_383 (or (and ?v_170 (and (and (not ?v_382) (= (ite ?v_375 ?v_95 ?v_381) ?v_179)) ?v_225)) ?v_382))) (or (and ?v_374 ?v_290) (and ?v_383 (or (and ?v_170 (and (and (not ?v_390) (= (ite ?v_375 ?v_127 ?v_389) ?v_179)) ?v_225)) ?v_390)))) (not ?v_398)) (or ?v_374 (and (not (and (and ?v_233 (= ?v_373 ?v_53)) ?v_234)) ?v_397)))) ?v_398))) (and ?v_488 (or (and ?v_400 (and (and (not ?v_449) (= (ite ?v_402 ?v_249 ?v_414) ?v_415)) ?v_501)) ?v_449))) (or (and ?v_399 (or (and (not ?v_460) (or (and (and ?v_362 (= ?v_451 ?v_452)) (= ?v_461 ?v_88)) (and (not ?v_453) (or (and (and ?v_240 (= ?v_308 ?v_452)) (= ?v_454 ?v_53)) (and (not ?v_455) (or (and (and ?v_150 (= ?v_199 ?v_452)) (= ?v_456 ?v_41)) (and (not ?v_457) (or (and (and ?v_89 (= ?v_122 ?v_452)) (= ?v_458 BOOOB_46_init_rob_head)) (and (not ?v_459) (not (and ?v_37 (= ?v_46 ?v_452)))))))))))) (or (and (and ?v_268 (= ?v_280 ?v_462)) (and (and (and (or (and ?v_463 ?v_269) (and ?v_472 (or (and ?v_170 (and (and (not ?v_471) (= (ite ?v_464 ?v_95 ?v_470) ?v_179)) ?v_225)) ?v_471))) (or (and ?v_463 ?v_290) (and ?v_472 (or (and ?v_170 (and (and (not ?v_479) (= (ite ?v_464 ?v_127 ?v_478) ?v_179)) ?v_225)) ?v_479)))) (not ?v_487)) (or ?v_463 (and (not (and (and ?v_233 (= ?v_462 ?v_53)) ?v_234)) ?v_486)))) ?v_487))) (and ?v_488 (or (and ?v_400 (and (and (not ?v_502) (= (ite ?v_402 ?v_317 ?v_500) ?v_415)) ?v_501)) ?v_502)))) (not ?v_516)) (or ?v_399 (and (not (and (and ?v_513 (= ?v_361 ?v_149)) ?v_514)) ?v_515)))) ?v_516))) (?v_519 (BOOOB_46_Decode_dest ?v_20)) (?v_520 (BOOOB_46_Decode_dest ?v_19))) (let ((?v_539 (ite (and ?v_517 (= ?v_361 ?v_518)) ?v_519 (ite ?v_399 ?v_520 (ite ?v_402 ?v_450 (ite ?v_403 ?v_307 (ite ?v_404 ?v_198 (ite ?v_405 ?v_121 (ite ?v_406 ?v_72 (ite ?v_407 ?v_46 BOOOB_46_init_null_reg))))))))) (?v_521 (and ?v_517 (= ?v_519 Br1))) (?v_524 (and ?v_359 (= ?v_520 Br1))) (?v_527 (and ?v_237 (= ?v_450 Br1))) (?v_529 (and ?v_147 (= ?v_307 Br1))) (?v_531 (and ?v_86 (= ?v_198 Br1))) (?v_533 (and ?v_51 (= ?v_121 Br1))) (?v_535 (and ?v_38 (= ?v_72 Br1)))) (let ((?v_534 (ite ?v_535 ?v_39 BOOOB_46_init_rob_head))) (let ((?v_532 (ite ?v_533 ?v_52 ?v_534))) (let ((?v_530 (ite ?v_531 ?v_87 ?v_532))) (let ((?v_528 (ite ?v_529 ?v_148 ?v_530))) (let ((?v_526 (ite ?v_527 ?v_238 ?v_528))) (let ((?v_523 (ite ?v_524 ?v_360 ?v_526))) (let ((?v_556 (ite ?v_521 ?v_518 ?v_523)) (?v_541 (ite (and ?v_359 (= ?v_239 ?v_360)) ?v_520 (ite ?v_267 ?v_450 (ite ?v_270 ?v_307 (ite ?v_271 ?v_198 (ite ?v_272 ?v_121 (ite ?v_273 ?v_72 (ite ?v_274 ?v_46 BOOOB_46_init_null_reg)))))))) (?v_544 (ite (and ?v_237 (= ?v_149 ?v_238)) ?v_450 (ite ?v_169 ?v_307 (ite ?v_172 ?v_198 (ite ?v_173 ?v_121 (ite ?v_174 ?v_72 (ite ?v_175 ?v_46 BOOOB_46_init_null_reg))))))) (?v_557 (and ?v_536 (= ?v_537 Br2))) (?v_540 (and ?v_517 (= ?v_519 Br2))) (?v_543 (and ?v_359 (= ?v_520 Br2))) (?v_546 (and ?v_237 (= ?v_450 Br2))) (?v_548 (and ?v_147 (= ?v_307 Br2))) (?v_550 (and ?v_86 (= ?v_198 Br2))) (?v_552 (and ?v_51 (= ?v_121 Br2))) (?v_554 (and ?v_38 (= ?v_72 Br2)))) (let ((?v_553 (ite ?v_554 ?v_39 BOOOB_46_init_rob_head))) (let ((?v_551 (ite ?v_552 ?v_52 ?v_553))) (let ((?v_549 (ite ?v_550 ?v_87 ?v_551))) (let ((?v_547 (ite ?v_548 ?v_148 ?v_549))) (let ((?v_545 (ite ?v_546 ?v_238 ?v_547))) (let ((?v_542 (ite ?v_543 ?v_360 ?v_545))) (let ((?v_559 (ite ?v_540 ?v_518 ?v_542)) (?v_558 (ite ?v_517 (+ 1 ?v_518) ?v_518))) (not (or (not (and (and (not (= Br1 Br2)) (not (and (not ?v_555) (or (and (and ?v_538 (= ?v_539 Br1)) (= ?v_556 ?v_361)) (and (not ?v_521) (or (and (and ?v_522 (= ?v_541 Br1)) (= ?v_523 ?v_239)) (and (not ?v_524) (or (and (and ?v_525 (= ?v_544 Br1)) (= ?v_526 ?v_149)) (and (not ?v_527) (or (and (and ?v_362 (= ?v_451 Br1)) (= ?v_528 ?v_88)) (and (not ?v_529) (or (and (and ?v_240 (= ?v_308 Br1)) (= ?v_530 ?v_53)) (and (not ?v_531) (or (and (and ?v_150 (= ?v_199 Br1)) (= ?v_532 ?v_41)) (and (not ?v_533) (or (and (and ?v_89 (= ?v_122 Br1)) (= ?v_534 BOOOB_46_init_rob_head)) (and (not ?v_535) (not (and ?v_37 (= ?v_46 Br1)))))))))))))))))))) (not (and (not ?v_557) (or (and (and ?v_538 (= ?v_539 Br2)) (= ?v_559 ?v_361)) (and (not ?v_540) (or (and (and ?v_522 (= ?v_541 Br2)) (= ?v_542 ?v_239)) (and (not ?v_543) (or (and (and ?v_525 (= ?v_544 Br2)) (= ?v_545 ?v_149)) (and (not ?v_546) (or (and (and ?v_362 (= ?v_451 Br2)) (= ?v_547 ?v_88)) (and (not ?v_548) (or (and (and ?v_240 (= ?v_308 Br2)) (= ?v_549 ?v_53)) (and (not ?v_550) (or (and (and ?v_150 (= ?v_199 Br2)) (= ?v_551 ?v_41)) (and (not ?v_552) (or (and (and ?v_89 (= ?v_122 Br2)) (= ?v_553 BOOOB_46_init_rob_head)) (and (not ?v_554) (not (and ?v_37 (= ?v_46 Br2))))))))))))))))))))) (not (= (ite ?v_555 ?v_558 ?v_556) (ite ?v_557 ?v_558 ?v_559))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress1/xs-11-20-5-2-5-3.smt2 b/test/regress/regress1/xs-11-20-5-2-5-3.smt2 new file mode 100644 index 000000000..bdf0d25ab --- /dev/null +++ b/test/regress/regress1/xs-11-20-5-2-5-3.smt2 @@ -0,0 +1,24 @@ +(set-logic QF_UFLIA) +(set-info :source | MathSat group |) +(set-info :smt-lib-version 2.0) +(set-info :category "industrial") +(set-info :status unsat) +(declare-fun fmt1 () Int) +(declare-fun fmt0 () Int) +(declare-fun arg1 () Int) +(declare-fun arg0 () Int) +(declare-fun fmt_length () Int) +(declare-fun distance () Int) +(declare-fun adr_hi () Int) +(declare-fun adr_medhi () Int) +(declare-fun adr_medlo () Int) +(declare-fun adr_lo () Int) +(declare-fun select_format (Int) Int) +(declare-fun percent () Int) +(declare-fun s () Int) +(declare-fun s_count (Int) Int) +(declare-fun x () Int) +(declare-fun x_count (Int) Int) +(assert (let ((?v_67 (+ fmt0 1)) (?v_0 (+ arg0 distance)) (?v_1 (- (- fmt1 2) fmt0)) (?v_2 (select_format 0))) (let ((?v_13 (= ?v_2 percent)) (?v_3 (select_format 1))) (let ((?v_16 (= ?v_3 percent)) (?v_14 (= ?v_3 s)) (?v_45 (= ?v_3 x)) (?v_4 (select_format 2))) (let ((?v_19 (= ?v_4 percent)) (?v_17 (= ?v_4 s)) (?v_47 (= ?v_4 x)) (?v_5 (select_format 3))) (let ((?v_22 (= ?v_5 percent)) (?v_20 (= ?v_5 s)) (?v_49 (= ?v_5 x)) (?v_6 (select_format 4))) (let ((?v_25 (= ?v_6 percent)) (?v_23 (= ?v_6 s)) (?v_51 (= ?v_6 x)) (?v_7 (select_format 5))) (let ((?v_28 (= ?v_7 percent)) (?v_26 (= ?v_7 s)) (?v_53 (= ?v_7 x)) (?v_8 (select_format 6))) (let ((?v_31 (= ?v_8 percent)) (?v_29 (= ?v_8 s)) (?v_55 (= ?v_8 x)) (?v_9 (select_format 7))) (let ((?v_34 (= ?v_9 percent)) (?v_32 (= ?v_9 s)) (?v_57 (= ?v_9 x)) (?v_10 (select_format 8))) (let ((?v_37 (= ?v_10 percent)) (?v_35 (= ?v_10 s)) (?v_59 (= ?v_10 x)) (?v_11 (select_format 9))) (let ((?v_40 (= ?v_11 percent)) (?v_38 (= ?v_11 s)) (?v_61 (= ?v_11 x)) (?v_12 (select_format 10))) (let ((?v_43 (= ?v_12 percent)) (?v_41 (= ?v_12 s)) (?v_63 (= ?v_12 x)) (?v_15 (s_count 0)) (?v_18 (s_count 1)) (?v_21 (s_count 2)) (?v_24 (s_count 3)) (?v_27 (s_count 4)) (?v_30 (s_count 5)) (?v_33 (s_count 6)) (?v_36 (s_count 7)) (?v_39 (s_count 8)) (?v_42 (s_count 9)) (?v_65 (select_format 11)) (?v_44 (s_count 10)) (?v_46 (x_count 0)) (?v_48 (x_count 1)) (?v_50 (x_count 2)) (?v_52 (x_count 3)) (?v_54 (x_count 4)) (?v_56 (x_count 5)) (?v_58 (x_count 6)) (?v_60 (x_count 7)) (?v_62 (x_count 8)) (?v_64 (x_count 9)) (?v_66 (x_count 10)) (?v_68 (+ fmt0 0)) (?v_69 (+ fmt0 2)) (?v_70 (+ fmt0 3)) (?v_71 (+ fmt0 4)) (?v_72 (+ fmt0 5)) (?v_73 (+ fmt0 6)) (?v_74 (+ fmt0 7))) (and (and (and (and (and (and (and (and (and (and (and (and (and (= distance 20) (= fmt_length 11)) (= adr_lo 5)) (= adr_medlo 2)) (= adr_medhi 5)) (= adr_hi 3)) (= percent 37)) (= s 115)) (= x 120)) (and (and (and (and (and (and (and (= fmt0 0) (= arg0 (- fmt0 distance))) (>= arg1 fmt0)) (< fmt1 (- (+ fmt0 fmt_length) 1))) (> fmt1 ?v_67)) (>= arg1 ?v_0)) (< arg1 (- (+ ?v_0 fmt_length) 4))) (= arg1 (+ (+ arg0 (* 4 (s_count ?v_1))) (* 4 (x_count ?v_1)))))) (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or (or ?v_13 (= ?v_2 s)) (= ?v_2 x)) (= ?v_2 adr_lo)) (= ?v_2 adr_medlo)) (= ?v_2 adr_medhi)) (= ?v_2 adr_hi)) (= ?v_2 255)) ?v_16) ?v_14) ?v_45) (= ?v_3 adr_lo)) (= ?v_3 adr_medlo)) (= ?v_3 adr_medhi)) (= ?v_3 adr_hi)) (= ?v_3 255)) ?v_19) ?v_17) ?v_47) (= ?v_4 adr_lo)) (= ?v_4 adr_medlo)) (= ?v_4 adr_medhi)) (= ?v_4 adr_hi)) (= ?v_4 255)) ?v_22) ?v_20) ?v_49) (= ?v_5 adr_lo)) (= ?v_5 adr_medlo)) (= ?v_5 adr_medhi)) (= ?v_5 adr_hi)) (= ?v_5 255)) ?v_25) ?v_23) ?v_51) (= ?v_6 adr_lo)) (= ?v_6 adr_medlo)) (= ?v_6 adr_medhi)) (= ?v_6 adr_hi)) (= ?v_6 255)) ?v_28) ?v_26) ?v_53) (= ?v_7 adr_lo)) (= ?v_7 adr_medlo)) (= ?v_7 adr_medhi)) (= ?v_7 adr_hi)) (= ?v_7 255)) ?v_31) ?v_29) ?v_55) (= ?v_8 adr_lo)) (= ?v_8 adr_medlo)) (= ?v_8 adr_medhi)) (= ?v_8 adr_hi)) (= ?v_8 255)) ?v_34) ?v_32) ?v_57) (= ?v_9 adr_lo)) (= ?v_9 adr_medlo)) (= ?v_9 adr_medhi)) (= ?v_9 adr_hi)) (= ?v_9 255)) ?v_37) ?v_35) ?v_59) (= ?v_10 adr_lo)) (= ?v_10 adr_medlo)) (= ?v_10 adr_medhi)) (= ?v_10 adr_hi)) (= ?v_10 255)) ?v_40) ?v_38) ?v_61) (= ?v_11 adr_lo)) (= ?v_11 adr_medlo)) (= ?v_11 adr_medhi)) (= ?v_11 adr_hi)) (= ?v_11 255)) ?v_43) ?v_41) ?v_63) (= ?v_12 adr_lo)) (= ?v_12 adr_medlo)) (= ?v_12 adr_medhi)) (= ?v_12 adr_hi)) (= ?v_12 255))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (ite (and ?v_13 ?v_14) (= ?v_15 1) (= ?v_15 0)) (ite (and ?v_16 ?v_17) (= ?v_18 (+ ?v_15 1)) (= ?v_18 ?v_15))) (ite (and ?v_19 ?v_20) (= ?v_21 (+ ?v_18 1)) (= ?v_21 ?v_18))) (ite (and ?v_22 ?v_23) (= ?v_24 (+ ?v_21 1)) (= ?v_24 ?v_21))) (ite (and ?v_25 ?v_26) (= ?v_27 (+ ?v_24 1)) (= ?v_27 ?v_24))) (ite (and ?v_28 ?v_29) (= ?v_30 (+ ?v_27 1)) (= ?v_30 ?v_27))) (ite (and ?v_31 ?v_32) (= ?v_33 (+ ?v_30 1)) (= ?v_33 ?v_30))) (ite (and ?v_34 ?v_35) (= ?v_36 (+ ?v_33 1)) (= ?v_36 ?v_33))) (ite (and ?v_37 ?v_38) (= ?v_39 (+ ?v_36 1)) (= ?v_39 ?v_36))) (ite (and ?v_40 ?v_41) (= ?v_42 (+ ?v_39 1)) (= ?v_42 ?v_39))) (ite (and ?v_43 (= ?v_65 s)) (= ?v_44 (+ ?v_42 1)) (= ?v_44 ?v_42))) (ite (and ?v_13 ?v_45) (= ?v_46 1) (= ?v_46 0))) (ite (and ?v_16 ?v_47) (= ?v_48 (+ ?v_46 1)) (= ?v_48 ?v_46))) (ite (and ?v_19 ?v_49) (= ?v_50 (+ ?v_48 1)) (= ?v_50 ?v_48))) (ite (and ?v_22 ?v_51) (= ?v_52 (+ ?v_50 1)) (= ?v_52 ?v_50))) (ite (and ?v_25 ?v_53) (= ?v_54 (+ ?v_52 1)) (= ?v_54 ?v_52))) (ite (and ?v_28 ?v_55) (= ?v_56 (+ ?v_54 1)) (= ?v_56 ?v_54))) (ite (and ?v_31 ?v_57) (= ?v_58 (+ ?v_56 1)) (= ?v_58 ?v_56))) (ite (and ?v_34 ?v_59) (= ?v_60 (+ ?v_58 1)) (= ?v_60 ?v_58))) (ite (and ?v_37 ?v_61) (= ?v_62 (+ ?v_60 1)) (= ?v_62 ?v_60))) (ite (and ?v_40 ?v_63) (= ?v_64 (+ ?v_62 1)) (= ?v_64 ?v_62))) (ite (and ?v_43 (= ?v_65 x)) (= ?v_66 (+ ?v_64 1)) (= ?v_66 ?v_64)))) (and (or (or (or (or (or (or (or (or (or (or (= fmt1 ?v_68) (= fmt1 ?v_67)) (= fmt1 ?v_69)) (= fmt1 ?v_70)) (= fmt1 ?v_71)) (= fmt1 ?v_72)) (= fmt1 ?v_73)) (= fmt1 ?v_74)) (= fmt1 (+ fmt0 8))) (= fmt1 (+ fmt0 9))) (= fmt1 (+ fmt0 10))) (or (or (or (or (or (or (or (= arg1 ?v_68) (= arg1 ?v_67)) (= arg1 ?v_69)) (= arg1 ?v_70)) (= arg1 ?v_71)) (= arg1 ?v_72)) (= arg1 ?v_73)) (= arg1 ?v_74)))) (not (and (and (and (and (and (= (select_format fmt1) percent) (= (select_format (+ fmt1 1)) s)) (= (select_format arg1) adr_lo)) (= (select_format (+ arg1 1)) adr_medlo)) (= (select_format (+ arg1 2)) adr_medhi)) (= (select_format (+ arg1 3)) adr_hi))))))))))))))))) +(check-sat) +(exit) -- 2.30.2