diff options
Diffstat (limited to 'test/regress/regress0/quantifiers/psyco-196.smt2')
| -rw-r--r-- | test/regress/regress0/quantifiers/psyco-196.smt2 | 422 |
1 files changed, 0 insertions, 422 deletions
diff --git a/test/regress/regress0/quantifiers/psyco-196.smt2 b/test/regress/regress0/quantifiers/psyco-196.smt2 deleted file mode 100644 index fef1a24c6..000000000 --- a/test/regress/regress0/quantifiers/psyco-196.smt2 +++ /dev/null @@ -1,422 +0,0 @@ -; COMMAND-LINE: --no-check-models -; EXPECT: sat -(set-logic LIA) -(set-info :status sat) -(declare-fun W_S1_V5 () Bool) -(declare-fun W_S1_V4 () Bool) -(declare-fun W_S1_V6 () Bool) -(declare-fun W_S1_V1 () Bool) -(declare-fun W_S1_V3 () Bool) -(declare-fun W_S1_V2 () Bool) -(declare-fun R_S1_V5 () Bool) -(declare-fun R_S1_V4 () Bool) -(declare-fun R_S1_V6 () Bool) -(declare-fun R_S1_V1 () Bool) -(declare-fun R_S1_V3 () Bool) -(declare-fun R_S1_V2 () Bool) -(declare-fun R_E2_V1 () Bool) -(declare-fun R_E1_V1 () Bool) -(declare-fun R_E1_V3 () Bool) -(declare-fun R_E2_V3 () Bool) -(assert - (let - (($x62242 - (forall - ((V2_0 Int) (V6_0 Int) - (V4_0 Int) (V5_0 Int) - (S1_V3_!5556 Int) (S1_V3_!5562 Int) - (S1_V3_!5571 Int) (S1_V3_!5577 Int) - (E1_!5552 Int) (E1_!5567 Int) - (E1_!5569 Int) (S1_V2_!5555 Int) - (S1_V2_!5561 Int) (S1_V2_!5570 Int) - (S1_V2_!5576 Int) (S1_V5_!5560 Int) - (S1_V5_!5566 Int) (S1_V5_!5575 Int) - (S1_V5_!5581 Int) (S1_V4_!5559 Int) - (S1_V4_!5565 Int) (S1_V4_!5574 Int) - (S1_V4_!5580 Int) (S1_V6_!5558 Int) - (S1_V6_!5564 Int) (S1_V6_!5573 Int) - (S1_V6_!5579 Int) (E2_!5553 Int) - (E2_!5554 Int) (E2_!5568 Int) - (S1_V1_!5557 Int) (S1_V1_!5563 Int) - (S1_V1_!5572 Int) (S1_V1_!5578 Int)) - (let (($x59864 (= S1_V5_!5566 S1_V5_!5581))) - (let (($x59925 (not W_S1_V5))) - (let (($x62779 (or $x59925 $x59864))) - (let (($x62200 (= S1_V4_!5565 S1_V4_!5580))) - (let (($x59923 (not W_S1_V4))) - (let (($x62447 (or $x59923 $x62200))) - (let (($x62602 (= S1_V6_!5564 S1_V6_!5579))) - (let (($x62610 (not W_S1_V6))) - (let (($x62230 (or $x62610 $x62602))) - (let (($x61214 (= S1_V1_!5563 S1_V1_!5578))) - (let (($x60986 (= S1_V3_!5562 S1_V3_!5577))) - (let (($x62444 (= S1_V2_!5561 S1_V2_!5576))) - (let (($x62507 (not W_S1_V2))) - (let (($x62441 (or $x62507 $x62444))) - (let - (($x62532 - (and $x62441 - (ite W_S1_V3 $x60986 - (= (ite W_S1_V3 S1_V3_!5556 E2_!5554) (+ (- 1) E2_!5568))) - (ite W_S1_V1 $x61214 - (= E1_!5552 (+ 1 (ite W_S1_V1 S1_V1_!5572 E1_!5569)))) $x62230 $x62447 - $x62779))) - (let ((?x62367 (ite W_S1_V1 S1_V1_!5572 E1_!5569))) - (let ((?x60865 (+ 1 ?x62367))) - (let ((?x62511 (ite W_S1_V1 S1_V1_!5578 ?x60865))) - (let ((?x60218 (ite W_S1_V3 S1_V3_!5556 E2_!5554))) - (let ((?x60222 (+ 1 ?x60218))) - (let ((?x62533 (ite W_S1_V3 S1_V3_!5562 ?x60222))) - (let - (($x62746 - (and (not (<= V4_0 E2_!5553)) - (not (<= V2_0 E1_!5552)) - (not (<= V4_0 E2_!5554)) - (not (<= (ite W_S1_V4 S1_V4_!5559 V4_0) ?x60222)) - (>= ?x62533 (+ (- 1) (ite W_S1_V4 S1_V4_!5565 V4_0))) - (>= (ite W_S1_V1 S1_V1_!5563 E1_!5552) - (+ (- 1) (ite W_S1_V2 S1_V2_!5561 V2_0))) - (not (<= V2_0 E1_!5567)) - (not (<= V4_0 E2_!5568)) - (not (<= V2_0 E1_!5569)) - (not (<= (ite W_S1_V2 S1_V2_!5570 V2_0) ?x60865)) - (>= ?x62511 (+ (- 1) (ite W_S1_V2 S1_V2_!5576 V2_0))) - (>= (ite W_S1_V3 S1_V3_!5577 E2_!5568) - (+ (- 1) (ite W_S1_V4 S1_V4_!5580 V4_0)))))) - (let (($x62780 (= S1_V1_!5578 S1_V1_!5572))) - (let (($x161 (not R_S1_V5))) - (let (($x62589 (or $x161 (= (ite W_S1_V5 S1_V5_!5575 V5_0) V5_0)))) - (let (($x159 (not R_S1_V4))) - (let (($x62548 (or $x159 (= (ite W_S1_V4 S1_V4_!5574 V4_0) V4_0)))) - (let (($x157 (not R_S1_V6))) - (let (($x62737 (or $x157 (= (ite W_S1_V6 S1_V6_!5573 V6_0) V6_0)))) - (let (($x153 (not R_S1_V3))) - (let - (($x62224 (or $x153 (= (ite W_S1_V3 S1_V3_!5571 E2_!5568) E2_!5568)))) - (let (($x151 (not R_S1_V2))) - (let (($x62641 (or $x151 (= (ite W_S1_V2 S1_V2_!5570 V2_0) V2_0)))) - (let - (($x60228 - (and $x62641 $x62224 - (or (not R_S1_V1) (= ?x62367 (+ (- 1) E1_!5569))) $x62737 $x62548 - $x62589))) - (let (($x62356 (not $x60228))) - (let (($x62680 (= S1_V1_!5578 S1_V1_!5563))) - (let (($x62272 (or $x161 $x59925 (= S1_V5_!5575 S1_V5_!5560)))) - (let (($x61083 (= S1_V4_!5574 S1_V4_!5559))) - (let (($x62455 (or $x159 $x59923 $x61083))) - (let (($x60917 (= S1_V6_!5573 S1_V6_!5558))) - (let (($x62584 (or $x157 $x62610 $x60917))) - (let (($x59905 (= S1_V2_!5570 S1_V2_!5555))) - (let (($x62549 (or $x151 $x62507 $x59905))) - (let - (($x62675 - (and $x62549 (or $x153 (= (ite W_S1_V3 S1_V3_!5571 E2_!5568) ?x60222)) - (or (not R_S1_V1) - (= ?x62367 (+ (- 1) (ite W_S1_V1 S1_V1_!5557 E1_!5552)))) $x62584 - $x62455 $x62272))) - (let (($x59892 (= S1_V1_!5578 S1_V1_!5557))) - (let - (($x60942 (or $x153 (= (ite W_S1_V3 S1_V3_!5571 E2_!5568) E2_!5554)))) - (let - (($x62564 - (and $x62641 $x60942 - (or (not R_S1_V1) (= ?x62367 (+ (- 1) E1_!5552))) $x62737 $x62548 - $x62589))) - (let (($x59819 (not $x62564))) - (let (($x60234 (= S1_V1_!5563 S1_V1_!5572))) - (let (($x61232 (or $x161 (= (ite W_S1_V5 S1_V5_!5560 V5_0) V5_0)))) - (let (($x61254 (or $x159 (= (ite W_S1_V4 S1_V4_!5559 V4_0) V4_0)))) - (let (($x59994 (or $x157 (= (ite W_S1_V6 S1_V6_!5558 V6_0) V6_0)))) - (let (($x155 (not R_S1_V1))) - (let - (($x62420 (or $x155 (= (ite W_S1_V1 S1_V1_!5557 E1_!5552) E1_!5569)))) - (let (($x62368 (or $x151 (= (ite W_S1_V2 S1_V2_!5555 V2_0) V2_0)))) - (let - (($x62830 - (not - (and $x62368 (or $x153 (= ?x60218 (+ (- 1) E2_!5568))) $x62420 $x59994 - $x61254 $x61232)))) - (let (($x62636 (= S1_V1_!5563 S1_V1_!5557))) - (let - (($x59733 (or $x155 (= (ite W_S1_V1 S1_V1_!5557 E1_!5552) E1_!5552)))) - (let - (($x62306 - (not - (and $x62368 (or $x153 (= ?x60218 (+ (- 1) E2_!5554))) $x59733 $x59994 - $x61254 $x61232)))) - (let (($x60134 (= S1_V1_!5557 S1_V1_!5572))) - (let - (($x59719 - (not - (and (or $x153 (= E2_!5554 E2_!5568)) (or $x155 (= E1_!5552 E1_!5569)))))) - (let (($x61406 (= E2_!5554 E2_!5568))) - (let (($x59878 (not (or (not R_E2_V1) (= E1_!5552 E1_!5567))))) - (let (($x59949 (or $x59878 $x61406))) - (let (($x62775 (or $x59878 (= E2_!5553 E2_!5568)))) - (let (($x59743 (= E2_!5553 E2_!5554))) - (let (($x62428 (= S1_V6_!5573 S1_V6_!5579))) - (let (($x60152 (or $x161 (= V5_0 (ite W_S1_V5 S1_V5_!5575 V5_0))))) - (let (($x60212 (or $x159 (= V4_0 (ite W_S1_V4 S1_V4_!5574 V4_0))))) - (let (($x61260 (or $x157 (= V6_0 (ite W_S1_V6 S1_V6_!5573 V6_0))))) - (let - (($x60887 (or $x153 (= E2_!5568 (ite W_S1_V3 S1_V3_!5571 E2_!5568))))) - (let (($x62275 (or $x151 (= V2_0 (ite W_S1_V2 S1_V2_!5570 V2_0))))) - (let - (($x61258 - (or - (not - (and $x62275 $x60887 - (or $x155 (= E1_!5569 ?x60865)) $x61260 $x60212 $x60152)) $x62428))) - (let - (($x61266 - (not - (and (or $x153 (= E2_!5568 E2_!5554)) (or $x155 (= E1_!5569 E1_!5552)))))) - (let (($x61122 (= S1_V5_!5560 S1_V5_!5575))) - (let (($x59790 (or $x161 $x59925 $x61122))) - (let (($x62797 (or $x159 $x59923 (= S1_V4_!5559 S1_V4_!5574)))) - (let (($x62684 (or $x157 $x62610 (= S1_V6_!5558 S1_V6_!5573)))) - (let (($x62354 (or $x151 $x62507 (= S1_V2_!5555 S1_V2_!5570)))) - (let - (($x60910 - (and $x62354 - (or $x153 (= ?x60218 (+ (- 1) (ite W_S1_V3 S1_V3_!5571 E2_!5568)))) - (or $x155 (= (ite W_S1_V1 S1_V1_!5557 E1_!5552) ?x60865)) $x62684 - $x62797 $x59790))) - (let (($x59844 (not $x60910))) - (let (($x62494 (= S1_V5_!5560 S1_V5_!5581))) - (let - (($x62623 (or $x153 (= E2_!5554 (ite W_S1_V3 S1_V3_!5571 E2_!5568))))) - (let - (($x61100 - (or - (not - (and $x62275 $x62623 - (or $x155 (= E1_!5552 ?x60865)) $x61260 $x60212 $x60152)) $x62494))) - (let (($x60862 (= S1_V5_!5560 S1_V5_!5566))) - (let (($x62353 (or $x161 (= V5_0 (ite W_S1_V5 S1_V5_!5560 V5_0))))) - (let (($x60875 (or $x159 (= V4_0 (ite W_S1_V4 S1_V4_!5559 V4_0))))) - (let (($x62491 (or $x157 (= V6_0 (ite W_S1_V6 S1_V6_!5558 V6_0))))) - (let - (($x62399 (or $x155 (= E1_!5552 (ite W_S1_V1 S1_V1_!5557 E1_!5552))))) - (let (($x62431 (or $x151 (= V2_0 (ite W_S1_V2 S1_V2_!5555 V2_0))))) - (let - (($x62297 - (or - (not - (and $x62431 (or $x153 (= E2_!5554 ?x60222)) $x62399 $x62491 $x60875 - $x62353)) $x60862))) - (let (($x60874 (= S1_V2_!5570 S1_V2_!5576))) - (let - (($x62369 - (or - (not - (and $x62275 $x60887 - (or $x155 (= E1_!5569 ?x60865)) $x61260 $x60212 $x60152)) $x60874))) - (let (($x62594 (= S1_V2_!5555 S1_V2_!5576))) - (let - (($x59910 - (or - (not - (and $x62275 $x62623 - (or $x155 (= E1_!5552 ?x60865)) $x61260 $x60212 $x60152)) $x62594))) - (let (($x62531 (= E1_!5569 E1_!5567))) - (let (($x59835 (= E1_!5552 E1_!5569))) - (let (($x62312 (= E1_!5552 E1_!5567))) - (let - (($x62715 - (and (or $x59719 (= S1_V3_!5556 S1_V3_!5571)) - (or $x62306 (= S1_V3_!5562 S1_V3_!5556)) - (or $x62830 (= S1_V3_!5562 S1_V3_!5571)) - (or $x59819 (= S1_V3_!5577 S1_V3_!5556)) - (or (not $x62675) (= S1_V3_!5577 S1_V3_!5562)) - (or $x62356 (= S1_V3_!5577 S1_V3_!5571)) $x62312 $x59835 $x62531 - $x59910 (or $x62306 (= S1_V2_!5561 S1_V2_!5555)) - (or $x62830 (= S1_V2_!5561 S1_V2_!5570)) - (or $x59844 $x62444) - (or $x61266 $x59905) $x62369 $x62297 - (or $x59719 $x61122) $x61100 - (or $x62830 (= S1_V5_!5566 S1_V5_!5575)) - (or $x59844 $x59864) - (or $x62356 (= S1_V5_!5581 S1_V5_!5575)) - (or $x62306 (= S1_V4_!5565 S1_V4_!5559)) - (or $x62830 (= S1_V4_!5565 S1_V4_!5574)) - (or $x59844 $x62200) - (or $x61266 $x61083) - (or $x59819 (= S1_V4_!5580 S1_V4_!5559)) - (or $x62356 (= S1_V4_!5580 S1_V4_!5574)) - (or $x62306 (= S1_V6_!5564 S1_V6_!5558)) - (or $x62830 (= S1_V6_!5564 S1_V6_!5573)) - (or $x59844 $x62602) - (or $x61266 $x60917) $x61258 - (or $x59819 (= S1_V6_!5579 S1_V6_!5558)) $x59743 $x62775 $x59949 - (or $x59719 $x60134) - (or $x62306 $x62636) - (or $x62830 $x60234) - (or $x59819 $x59892) - (or (not $x62675) $x62680) - (or $x62356 $x62780)))) - (or (not $x62715) (not $x62746) $x62532))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - (let (($x13 (or W_S1_V2 W_S1_V3 W_S1_V1 W_S1_V6 W_S1_V4 W_S1_V5))) - (let (($x65 (not R_E1_V1))) - (let (($x63 (not R_E1_V3))) - (let (($x84 (not R_E2_V3))) (and $x84 $x63 $x65 $x13 $x62242))))))) -(assert (not (and (not W_S1_V4) (not W_S1_V3)))) -(assert (not (and (not W_S1_V1) (not W_S1_V2)))) -(assert (not (and (not R_S1_V3) (not R_S1_V1) (not W_S1_V4) (not W_S1_V2)))) -(assert - (let (($x62714 (not W_S1_V3))) - (let (($x161 (not R_S1_V5))) - (let (($x159 (not R_S1_V4))) - (let (($x157 (not R_S1_V6))) - (let (($x155 (not R_S1_V1))) - (let (($x151 (not R_S1_V2))) - (not (and $x151 $x155 $x157 $x159 $x161 $x62714))))))))) -(assert - (let (($x62610 (not W_S1_V6))) - (let (($x62507 (not W_S1_V2))) - (let (($x59925 (not W_S1_V5))) - (let (($x159 (not R_S1_V4))) - (let (($x155 (not R_S1_V1))) - (let (($x153 (not R_S1_V3))) - (not (and $x153 $x155 $x159 $x59925 $x62507 $x62610))))))))) -(assert - (let (($x161 (not R_S1_V5))) - (let (($x159 (not R_S1_V4))) - (let (($x157 (not R_S1_V6))) - (let (($x155 (not R_S1_V1))) - (let (($x153 (not R_S1_V3))) - (let (($x151 (not R_S1_V2))) - (not (and $x151 $x153 $x155 $x157 $x159 $x161))))))))) -(assert (not (and W_S1_V3 (not R_S1_V3) (not R_S1_V1) (not W_S1_V2)))) -(assert (not (and W_S1_V3 W_S1_V1 (not R_S1_V3) (not R_S1_V1)))) -(assert - (let (($x62232 (not W_S1_V1))) - (let (($x59925 (not W_S1_V5))) - (let (($x159 (not R_S1_V4))) - (let (($x157 (not R_S1_V6))) - (let (($x153 (not R_S1_V3))) - (let (($x151 (not R_S1_V2))) - (not (and $x151 $x153 $x157 $x159 $x59925 $x62232))))))))) -(assert - (let (($x62610 (not W_S1_V6))) - (let (($x62232 (not W_S1_V1))) - (let (($x59925 (not W_S1_V5))) - (let (($x159 (not R_S1_V4))) - (let (($x153 (not R_S1_V3))) - (let (($x151 (not R_S1_V2))) - (not (and $x151 $x153 $x159 $x59925 $x62232 $x62610))))))))) -(assert - (let (($x62610 (not W_S1_V6))) - (let (($x59923 (not W_S1_V4))) - (let (($x161 (not R_S1_V5))) - (let (($x155 (not R_S1_V1))) - (let (($x153 (not R_S1_V3))) - (let (($x151 (not R_S1_V2))) - (not (and $x151 $x153 $x155 $x161 $x59923 $x62610))))))))) -(assert - (let (($x62610 (not W_S1_V6))) - (let (($x62232 (not W_S1_V1))) - (let (($x161 (not R_S1_V5))) - (let (($x159 (not R_S1_V4))) - (let (($x153 (not R_S1_V3))) - (let (($x151 (not R_S1_V2))) - (not (and $x151 $x153 $x159 $x161 $x62232 $x62610))))))))) -(assert - (let (($x62232 (not W_S1_V1))) - (let (($x59925 (not W_S1_V5))) - (let (($x59923 (not W_S1_V4))) - (let (($x157 (not R_S1_V6))) - (let (($x153 (not R_S1_V3))) - (let (($x151 (not R_S1_V2))) - (not (and $x151 $x153 $x157 $x59923 $x59925 $x62232))))))))) -(assert - (let (($x62610 (not W_S1_V6))) - (let (($x59925 (not W_S1_V5))) - (let (($x59923 (not W_S1_V4))) - (let (($x155 (not R_S1_V1))) - (let (($x153 (not R_S1_V3))) - (let (($x151 (not R_S1_V2))) - (not (and $x151 $x153 $x155 $x59923 $x59925 $x62610))))))))) -(assert - (let (($x59923 (not W_S1_V4))) - (let (($x161 (not R_S1_V5))) - (let (($x157 (not R_S1_V6))) - (let (($x155 (not R_S1_V1))) - (let (($x153 (not R_S1_V3))) - (let (($x151 (not R_S1_V2))) - (not (and $x151 $x153 $x155 $x157 $x161 $x59923))))))))) -(assert - (let (($x62232 (not W_S1_V1))) - (let (($x59923 (not W_S1_V4))) - (let (($x161 (not R_S1_V5))) - (let (($x157 (not R_S1_V6))) - (let (($x153 (not R_S1_V3))) - (let (($x151 (not R_S1_V2))) - (not (and $x151 $x153 $x157 $x161 $x59923 $x62232))))))))) -(assert - (let (($x62714 (not W_S1_V3))) - (let (($x62507 (not W_S1_V2))) - (let (($x161 (not R_S1_V5))) - (let (($x159 (not R_S1_V4))) - (let (($x157 (not R_S1_V6))) - (let (($x155 (not R_S1_V1))) - (not (and $x155 $x157 $x159 $x161 $x62507 $x62714))))))))) -(assert - (let (($x62714 (not W_S1_V3))) - (let (($x62610 (not W_S1_V6))) - (let (($x161 (not R_S1_V5))) - (let (($x159 (not R_S1_V4))) - (let (($x155 (not R_S1_V1))) - (let (($x151 (not R_S1_V2))) - (not (and $x151 $x155 $x159 $x161 $x62610 $x62714))))))))) -(assert - (let (($x62714 (not W_S1_V3))) - (let (($x62610 (not W_S1_V6))) - (let (($x62507 (not W_S1_V2))) - (let (($x161 (not R_S1_V5))) - (let (($x159 (not R_S1_V4))) - (let (($x155 (not R_S1_V1))) - (not (and $x155 $x159 $x161 $x62507 $x62610 $x62714))))))))) -(assert - (let (($x62714 (not W_S1_V3))) - (let (($x59925 (not W_S1_V5))) - (let (($x159 (not R_S1_V4))) - (let (($x157 (not R_S1_V6))) - (let (($x155 (not R_S1_V1))) - (let (($x151 (not R_S1_V2))) - (not (and $x151 $x155 $x157 $x159 $x59925 $x62714))))))))) -(assert - (let (($x62714 (not W_S1_V3))) - (let (($x62507 (not W_S1_V2))) - (let (($x59925 (not W_S1_V5))) - (let (($x159 (not R_S1_V4))) - (let (($x157 (not R_S1_V6))) - (let (($x155 (not R_S1_V1))) - (not (and $x155 $x157 $x159 $x59925 $x62507 $x62714))))))))) -(assert - (let (($x62714 (not W_S1_V3))) - (let (($x62610 (not W_S1_V6))) - (let (($x59925 (not W_S1_V5))) - (let (($x159 (not R_S1_V4))) - (let (($x155 (not R_S1_V1))) - (let (($x151 (not R_S1_V2))) - (not (and $x151 $x155 $x159 $x59925 $x62610 $x62714))))))))) -(assert - (let (($x62714 (not W_S1_V3))) - (let (($x62610 (not W_S1_V6))) - (let (($x62507 (not W_S1_V2))) - (let (($x59925 (not W_S1_V5))) - (let (($x159 (not R_S1_V4))) - (let (($x155 (not R_S1_V1))) - (not (and $x155 $x159 $x59925 $x62507 $x62610 $x62714))))))))) -(assert - (let (($x62232 (not W_S1_V1))) - (let (($x161 (not R_S1_V5))) - (let (($x159 (not R_S1_V4))) - (let (($x157 (not R_S1_V6))) - (let (($x153 (not R_S1_V3))) - (let (($x151 (not R_S1_V2))) - (not (and $x151 $x153 $x157 $x159 $x161 $x62232))))))))) -(check-sat) - |