diff options
Diffstat (limited to 'test/regress/regress1/quantifiers/psyco-196.smt2')
| -rw-r--r-- | test/regress/regress1/quantifiers/psyco-196.smt2 | 422 |
1 files changed, 422 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/psyco-196.smt2 b/test/regress/regress1/quantifiers/psyco-196.smt2 new file mode 100644 index 000000000..fef1a24c6 --- /dev/null +++ b/test/regress/regress1/quantifiers/psyco-196.smt2 @@ -0,0 +1,422 @@ +; 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) + |