Skip to content
Snippets Groups Projects
Commit 2dca0978 authored by Bruno Marre's avatar Bruno Marre Committed by Christophe Junke
Browse files

menage

parent e1544d8e
No related branches found
No related tags found
1 merge request!55Update and fix tests
Hide whitespace changes
Inline Side-by-side
UnitTests/sat/QF_NIA/From_AProVE_2014__PastaA10.jar-obl-8__p11616_terminationG_0.smt2 deleted 100644 → 0
+ 0
− 90
View file @ e1544d8e
(set-info :smt-lib-version 2.6)
(set-logic QF_NIA)
(set-info :source |
Generated by: Cristina Borralleras, Daniel Larraz, Albert Oliveras, Enric Rodriguez-Carbonell, Albert Rubio
Generated on: 2017-04-27
Generator: VeryMax
Application: Termination proving
Target solver: barcelogic
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status sat)
(declare-fun Nl2arg11 () Int)
(declare-fun Nl2arg21 () Int)
(declare-fun Nl2arg12 () Int)
(declare-fun Nl2arg22 () Int)
(declare-fun lam0n0 () Int)
(declare-fun lam0n1 () Int)
(declare-fun lam0n2 () Int)
(declare-fun Nl2CT1 () Int)
(declare-fun Nl2CT2 () Int)
(declare-fun lam1n0 () Int)
(declare-fun lam1n1 () Int)
(declare-fun lam1n2 () Int)
(declare-fun lam2n0 () Int)
(declare-fun lam2n1 () Int)
(declare-fun lam2n2 () Int)
(declare-fun lam3n0 () Int)
(declare-fun lam3n1 () Int)
(declare-fun lam3n2 () Int)
(declare-fun lam4n0 () Int)
(declare-fun lam4n1 () Int)
(declare-fun lam4n2 () Int)
(declare-fun lam5n0 () Int)
(declare-fun lam5n1 () Int)
(declare-fun lam5n2 () Int)
(declare-fun lam6n0 () Int)
(declare-fun lam6n1 () Int)
(declare-fun lam6n2 () Int)
(declare-fun lam6n3 () Int)
(declare-fun lam6n4 () Int)
(declare-fun lam6n5 () Int)
(declare-fun lam7n0 () Int)
(declare-fun lam7n1 () Int)
(declare-fun lam7n2 () Int)
(declare-fun lam7n3 () Int)
(declare-fun lam7n4 () Int)
(declare-fun lam7n5 () Int)
(declare-fun undef7 () Int)
(declare-fun undef1 () Int)
(declare-fun undef2 () Int)
(declare-fun undef8 () Int)
(declare-fun arg1 () Int)
(declare-fun arg2 () Int)
(declare-fun lam11n0 () Int)
(declare-fun lam11n1 () Int)
(declare-fun lam11n2 () Int)
(declare-fun RFN1_CT () Int)
(declare-fun RFN1_arg1 () Int)
(declare-fun RFN1_arg2 () Int)
(declare-fun lam15n0 () Int)
(declare-fun lam15n1 () Int)
(declare-fun lam15n2 () Int)
(declare-fun lam9n0 () Int)
(declare-fun lam9n1 () Int)
(declare-fun lam9n2 () Int)
(declare-fun lam10n0 () Int)
(declare-fun lam10n1 () Int)
(declare-fun lam10n2 () Int)
(declare-fun lam13n0 () Int)
(declare-fun lam13n1 () Int)
(declare-fun lam13n2 () Int)
(declare-fun lam14n0 () Int)
(declare-fun lam14n1 () Int)
(declare-fun lam14n2 () Int)
(declare-fun lam8n0 () Int)
(declare-fun lam8n1 () Int)
(declare-fun lam8n2 () Int)
(declare-fun lam12n0 () Int)
(declare-fun lam12n1 () Int)
(declare-fun lam12n2 () Int)
(assert ( and ( <= ( - 1 ) Nl2arg11 ) ( <= Nl2arg11 1 ) ( <= ( - 1 ) Nl2arg21 ) ( <= Nl2arg21 1 ) ( <= ( - 1 ) Nl2arg12 ) ( <= Nl2arg12 1 ) ( <= ( - 1 ) Nl2arg22 ) ( <= Nl2arg22 1 ) ))
(assert ( or ( and ( >= lam0n0 0 ) ( >= lam0n1 0 ) ( >= lam0n2 0 ) ( > ( + ( * 1 lam0n0 ) ( * Nl2CT1 lam0n1 ) ( * Nl2CT2 lam0n2 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * Nl2arg11 lam0n1 ) ( * Nl2arg12 lam0n2 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * Nl2arg21 lam0n1 ) ( * Nl2arg22 lam0n2 ) ) 0 ) ) ( and ( >= lam1n0 0 ) ( >= lam1n1 0 ) ( >= lam1n2 0 ) ( > ( + ( * 1 lam1n0 ) ( * Nl2CT1 lam1n1 ) ( * Nl2CT2 lam1n2 ) ( - 1 ( + Nl2CT1 ( * Nl2arg11 1 ) ) ) ) 0 ) ( = ( + ( * 1 lam1n0 ) ( * Nl2arg11 lam1n1 ) ( * Nl2arg12 lam1n2 ) ( - ( + 0 ( * Nl2arg11 1 ) ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam1n0 ) ( * Nl2arg21 lam1n1 ) ( * Nl2arg22 lam1n2 ) ( - ( + 0 Nl2arg21 ) ) ) 0 ) ) ))
(assert ( or ( and ( >= lam0n0 0 ) ( >= lam0n1 0 ) ( >= lam0n2 0 ) ( > ( + ( * 1 lam0n0 ) ( * Nl2CT1 lam0n1 ) ( * Nl2CT2 lam0n2 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * Nl2arg11 lam0n1 ) ( * Nl2arg12 lam0n2 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * Nl2arg21 lam0n1 ) ( * Nl2arg22 lam0n2 ) ) 0 ) ) ( and ( >= lam2n0 0 ) ( >= lam2n1 0 ) ( >= lam2n2 0 ) ( > ( + ( * 1 lam2n0 ) ( * Nl2CT1 lam2n1 ) ( * Nl2CT2 lam2n2 ) ( - 1 ( + Nl2CT2 ( * Nl2arg12 1 ) ) ) ) 0 ) ( = ( + ( * 1 lam2n0 ) ( * Nl2arg11 lam2n1 ) ( * Nl2arg12 lam2n2 ) ( - ( + 0 ( * Nl2arg12 1 ) ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam2n0 ) ( * Nl2arg21 lam2n1 ) ( * Nl2arg22 lam2n2 ) ( - ( + 0 Nl2arg22 ) ) ) 0 ) ) ))
(assert ( or ( and ( >= lam3n0 0 ) ( >= lam3n1 0 ) ( >= lam3n2 0 ) ( > ( + ( * 1 lam3n0 ) ( * Nl2CT1 lam3n1 ) ( * Nl2CT2 lam3n2 ) ( - 1 ) ) 0 ) ( = ( + ( * ( - 1 ) lam3n0 ) ( * Nl2arg11 lam3n1 ) ( * Nl2arg12 lam3n2 ) ) 0 ) ( = ( + ( * 1 lam3n0 ) ( * Nl2arg21 lam3n1 ) ( * Nl2arg22 lam3n2 ) ) 0 ) ) ( and ( >= lam4n0 0 ) ( >= lam4n1 0 ) ( >= lam4n2 0 ) ( > ( + ( * 1 lam4n0 ) ( * Nl2CT1 lam4n1 ) ( * Nl2CT2 lam4n2 ) ( - 1 ( + Nl2CT1 ( * Nl2arg21 1 ) ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam4n0 ) ( * Nl2arg11 lam4n1 ) ( * Nl2arg12 lam4n2 ) ( - ( + 0 Nl2arg11 ) ) ) 0 ) ( = ( + ( * 1 lam4n0 ) ( * Nl2arg21 lam4n1 ) ( * Nl2arg22 lam4n2 ) ( - ( + 0 ( * Nl2arg21 1 ) ) ) ) 0 ) ) ))
(assert ( or ( and ( >= lam3n0 0 ) ( >= lam3n1 0 ) ( >= lam3n2 0 ) ( > ( + ( * 1 lam3n0 ) ( * Nl2CT1 lam3n1 ) ( * Nl2CT2 lam3n2 ) ( - 1 ) ) 0 ) ( = ( + ( * ( - 1 ) lam3n0 ) ( * Nl2arg11 lam3n1 ) ( * Nl2arg12 lam3n2 ) ) 0 ) ( = ( + ( * 1 lam3n0 ) ( * Nl2arg21 lam3n1 ) ( * Nl2arg22 lam3n2 ) ) 0 ) ) ( and ( >= lam5n0 0 ) ( >= lam5n1 0 ) ( >= lam5n2 0 ) ( > ( + ( * 1 lam5n0 ) ( * Nl2CT1 lam5n1 ) ( * Nl2CT2 lam5n2 ) ( - 1 ( + Nl2CT2 ( * Nl2arg22 1 ) ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam5n0 ) ( * Nl2arg11 lam5n1 ) ( * Nl2arg12 lam5n2 ) ( - ( + 0 Nl2arg12 ) ) ) 0 ) ( = ( + ( * 1 lam5n0 ) ( * Nl2arg21 lam5n1 ) ( * Nl2arg22 lam5n2 ) ( - ( + 0 ( * Nl2arg22 1 ) ) ) ) 0 ) ) ))
(assert ( and ( <= ( + 1 ( * ( - 1 ) undef7 ) ) 0 ) ( <= ( * ( - 1 ) undef1 ) 0 ) ( <= ( * ( - 1 ) undef2 ) 0 ) ( <= ( * ( - 1 ) undef8 ) 0 ) ( = ( + arg1 ( * ( - 1 ) undef1 ) ) 0 ) ( = ( + arg2 ( * ( - 1 ) undef2 ) ) 0 ) ( <= ( + Nl2CT1 ( * ( + 0 Nl2arg11 ) arg1 ) ( * ( + 0 Nl2arg21 ) arg2 ) ) 0 ) ( <= ( + Nl2CT2 ( * ( + 0 Nl2arg12 ) arg1 ) ( * ( + 0 Nl2arg22 ) arg2 ) ) 0 ) ))
(assert ( or ( and ( and ( and ( >= lam11n0 0 ) ( >= lam11n1 0 ) ( >= lam11n2 0 ) ( > ( + ( * 1 lam11n0 ) ( * Nl2CT1 lam11n1 ) ( * Nl2CT2 lam11n2 ) ( - 1 ( - ( + RFN1_CT ( * RFN1_arg1 1 ) ) RFN1_CT ) ) ) 0 ) ( = ( + ( * 1 lam11n0 ) ( * Nl2arg11 lam11n1 ) ( * Nl2arg12 lam11n2 ) ( - ( - ( + 0 ( * RFN1_arg1 1 ) ) RFN1_arg1 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam11n0 ) ( * Nl2arg21 lam11n1 ) ( * Nl2arg22 lam11n2 ) ( - ( - ( + 0 RFN1_arg2 ) RFN1_arg2 ) ) ) 0 ) ) ( and ( >= lam15n0 0 ) ( >= lam15n1 0 ) ( >= lam15n2 0 ) ( > ( + ( * 1 lam15n0 ) ( * Nl2CT1 lam15n1 ) ( * Nl2CT2 lam15n2 ) ( - 1 ( - ( + RFN1_CT ( * RFN1_arg2 1 ) ) RFN1_CT ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam15n0 ) ( * Nl2arg11 lam15n1 ) ( * Nl2arg12 lam15n2 ) ( - ( - ( + 0 RFN1_arg1 ) RFN1_arg1 ) ) ) 0 ) ( = ( + ( * 1 lam15n0 ) ( * Nl2arg21 lam15n1 ) ( * Nl2arg22 lam15n2 ) ( - ( - ( + 0 ( * RFN1_arg2 1 ) ) RFN1_arg2 ) ) ) 0 ) ) ) ( or ( and ( and ( >= lam9n0 0 ) ( >= lam9n1 0 ) ( >= lam9n2 0 ) ( > ( + ( * 1 lam9n0 ) ( * Nl2CT1 lam9n1 ) ( * Nl2CT2 lam9n2 ) ( - 1 ( - RFN1_CT ) ) ) 0 ) ( = ( + ( * 1 lam9n0 ) ( * Nl2arg11 lam9n1 ) ( * Nl2arg12 lam9n2 ) ( - ( - RFN1_arg1 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam9n0 ) ( * Nl2arg21 lam9n1 ) ( * Nl2arg22 lam9n2 ) ( - ( - RFN1_arg2 ) ) ) 0 ) ) ( and ( >= lam10n0 0 ) ( >= lam10n1 0 ) ( >= lam10n2 0 ) ( > ( + ( * 1 lam10n0 ) ( * Nl2CT1 lam10n1 ) ( * Nl2CT2 lam10n2 ) ( - 1 ( + ( - ( + RFN1_CT ( * RFN1_arg1 1 ) ) RFN1_CT ) 1 ) ) ) 0 ) ( = ( + ( * 1 lam10n0 ) ( * Nl2arg11 lam10n1 ) ( * Nl2arg12 lam10n2 ) ( - ( - ( + 0 ( * RFN1_arg1 1 ) ) RFN1_arg1 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam10n0 ) ( * Nl2arg21 lam10n1 ) ( * Nl2arg22 lam10n2 ) ( - ( - ( + 0 RFN1_arg2 ) RFN1_arg2 ) ) ) 0 ) ) ) ( and ( and ( >= lam13n0 0 ) ( >= lam13n1 0 ) ( >= lam13n2 0 ) ( > ( + ( * 1 lam13n0 ) ( * Nl2CT1 lam13n1 ) ( * Nl2CT2 lam13n2 ) ( - 1 ( - RFN1_CT ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam13n0 ) ( * Nl2arg11 lam13n1 ) ( * Nl2arg12 lam13n2 ) ( - ( - RFN1_arg1 ) ) ) 0 ) ( = ( + ( * 1 lam13n0 ) ( * Nl2arg21 lam13n1 ) ( * Nl2arg22 lam13n2 ) ( - ( - RFN1_arg2 ) ) ) 0 ) ) ( and ( >= lam14n0 0 ) ( >= lam14n1 0 ) ( >= lam14n2 0 ) ( > ( + ( * 1 lam14n0 ) ( * Nl2CT1 lam14n1 ) ( * Nl2CT2 lam14n2 ) ( - 1 ( + ( - ( + RFN1_CT ( * RFN1_arg2 1 ) ) RFN1_CT ) 1 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam14n0 ) ( * Nl2arg11 lam14n1 ) ( * Nl2arg12 lam14n2 ) ( - ( - ( + 0 RFN1_arg1 ) RFN1_arg1 ) ) ) 0 ) ( = ( + ( * 1 lam14n0 ) ( * Nl2arg21 lam14n1 ) ( * Nl2arg22 lam14n2 ) ( - ( - ( + 0 ( * RFN1_arg2 1 ) ) RFN1_arg2 ) ) ) 0 ) ) ) ) ) ( or ( and ( >= lam8n0 0 ) ( >= lam8n1 0 ) ( >= lam8n2 0 ) ( > ( + ( * 1 lam8n0 ) ( * Nl2CT1 lam8n1 ) ( * Nl2CT2 lam8n2 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam8n0 ) ( * Nl2arg11 lam8n1 ) ( * Nl2arg12 lam8n2 ) ) 0 ) ( = ( + ( * ( - 1 ) lam8n0 ) ( * Nl2arg21 lam8n1 ) ( * Nl2arg22 lam8n2 ) ) 0 ) ) ( and ( >= lam12n0 0 ) ( >= lam12n1 0 ) ( >= lam12n2 0 ) ( > ( + ( * 1 lam12n0 ) ( * Nl2CT1 lam12n1 ) ( * Nl2CT2 lam12n2 ) ( - 1 ) ) 0 ) ( = ( + ( * ( - 1 ) lam12n0 ) ( * Nl2arg11 lam12n1 ) ( * Nl2arg12 lam12n2 ) ) 0 ) ( = ( + ( * 1 lam12n0 ) ( * Nl2arg21 lam12n1 ) ( * Nl2arg22 lam12n2 ) ) 0 ) ) ) ))
(check-sat)
(exit)
UnitTests/sat/QF_NIA/From_T2__consts3nt.t2__p18166_terminationG_0.smt2 deleted 100644 → 0
+ 0
− 74
View file @ e1544d8e
(set-info :smt-lib-version 2.6)
(set-logic QF_NIA)
(set-info :source |
Generated by: Cristina Borralleras, Daniel Larraz, Albert Oliveras, Enric Rodriguez-Carbonell, Albert Rubio
Generated on: 2017-04-27
Generator: VeryMax
Application: Termination proving
Target solver: barcelogic
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status sat)
(declare-fun Nl1__const_200^01 () Int)
(declare-fun Nl1x^01 () Int)
(declare-fun Nl1__const_200^02 () Int)
(declare-fun Nl1x^02 () Int)
(declare-fun Nl1__const_200^03 () Int)
(declare-fun Nl1x^03 () Int)
(declare-fun lam0n0 () Int)
(declare-fun lam0n2 () Int)
(declare-fun lam0n3 () Int)
(declare-fun lam0n4 () Int)
(declare-fun lam0n1 () Int)
(declare-fun Nl1CT1 () Int)
(declare-fun Nl1CT2 () Int)
(declare-fun Nl1CT3 () Int)
(declare-fun lam1n0 () Int)
(declare-fun lam1n2 () Int)
(declare-fun lam1n3 () Int)
(declare-fun lam1n4 () Int)
(declare-fun lam1n1 () Int)
(declare-fun lam2n0 () Int)
(declare-fun lam2n2 () Int)
(declare-fun lam2n3 () Int)
(declare-fun lam2n4 () Int)
(declare-fun lam2n1 () Int)
(declare-fun lam3n0 () Int)
(declare-fun lam3n2 () Int)
(declare-fun lam3n3 () Int)
(declare-fun lam3n4 () Int)
(declare-fun lam3n1 () Int)
(declare-fun __const_200^0 () Int)
(declare-fun x^0 () Int)
(declare-fun lam10n0 () Int)
(declare-fun lam10n2 () Int)
(declare-fun lam10n3 () Int)
(declare-fun lam10n4 () Int)
(declare-fun lam10n1 () Int)
(declare-fun RFN1_CT () Int)
(declare-fun RFN1_x^0 () Int)
(declare-fun RFN1___const_200^0 () Int)
(declare-fun lam8n0 () Int)
(declare-fun lam8n2 () Int)
(declare-fun lam8n3 () Int)
(declare-fun lam8n4 () Int)
(declare-fun lam8n1 () Int)
(declare-fun lam9n0 () Int)
(declare-fun lam9n2 () Int)
(declare-fun lam9n3 () Int)
(declare-fun lam9n4 () Int)
(declare-fun lam9n1 () Int)
(declare-fun lam7n0 () Int)
(declare-fun lam7n2 () Int)
(declare-fun lam7n3 () Int)
(declare-fun lam7n4 () Int)
(declare-fun lam7n1 () Int)
(assert ( and ( <= ( - 1 ) Nl1__const_200^01 ) ( <= Nl1__const_200^01 1 ) ( <= ( - 1 ) Nl1x^01 ) ( <= Nl1x^01 1 ) ( <= ( - 1 ) Nl1__const_200^02 ) ( <= Nl1__const_200^02 1 ) ( <= ( - 1 ) Nl1x^02 ) ( <= Nl1x^02 1 ) ( <= ( - 1 ) Nl1__const_200^03 ) ( <= Nl1__const_200^03 1 ) ( <= ( - 1 ) Nl1x^03 ) ( <= Nl1x^03 1 ) ))
(assert ( or ( and ( >= lam0n0 0 ) ( >= lam0n2 0 ) ( >= lam0n3 0 ) ( >= lam0n4 0 ) ( > ( + ( * 1 lam0n0 ) ( * 1 lam0n1 ) ( * Nl1CT1 lam0n2 ) ( * Nl1CT2 lam0n3 ) ( * Nl1CT3 lam0n4 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * Nl1__const_200^01 lam0n2 ) ( * Nl1__const_200^02 lam0n3 ) ( * Nl1__const_200^03 lam0n4 ) ) 0 ) ( = ( + ( * 1 lam0n1 ) ( * Nl1x^01 lam0n2 ) ( * Nl1x^02 lam0n3 ) ( * Nl1x^03 lam0n4 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * ( - 1 ) lam0n1 ) ) 0 ) ) ( and ( >= lam1n0 0 ) ( >= lam1n2 0 ) ( >= lam1n3 0 ) ( >= lam1n4 0 ) ( > ( + ( * 1 lam1n0 ) ( * 1 lam1n1 ) ( * Nl1CT1 lam1n2 ) ( * Nl1CT2 lam1n3 ) ( * Nl1CT3 lam1n4 ) ( - 1 ( + Nl1CT1 ( * Nl1x^01 0 ) ) ) ) 0 ) ( = ( + ( * 1 lam1n0 ) ( * Nl1__const_200^01 lam1n2 ) ( * Nl1__const_200^02 lam1n3 ) ( * Nl1__const_200^03 lam1n4 ) ( - ( + 0 Nl1__const_200^01 ) ) ) 0 ) ( = ( + ( * 1 lam1n1 ) ( * Nl1x^01 lam1n2 ) ( * Nl1x^02 lam1n3 ) ( * Nl1x^03 lam1n4 ) ) 0 ) ( = ( + ( * ( - 1 ) lam1n0 ) ( * ( - 1 ) lam1n1 ) ( - ( + 0 ( * Nl1x^01 1 ) ) ) ) 0 ) ) ))
(assert ( or ( and ( >= lam0n0 0 ) ( >= lam0n2 0 ) ( >= lam0n3 0 ) ( >= lam0n4 0 ) ( > ( + ( * 1 lam0n0 ) ( * 1 lam0n1 ) ( * Nl1CT1 lam0n2 ) ( * Nl1CT2 lam0n3 ) ( * Nl1CT3 lam0n4 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * Nl1__const_200^01 lam0n2 ) ( * Nl1__const_200^02 lam0n3 ) ( * Nl1__const_200^03 lam0n4 ) ) 0 ) ( = ( + ( * 1 lam0n1 ) ( * Nl1x^01 lam0n2 ) ( * Nl1x^02 lam0n3 ) ( * Nl1x^03 lam0n4 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * ( - 1 ) lam0n1 ) ) 0 ) ) ( and ( >= lam2n0 0 ) ( >= lam2n2 0 ) ( >= lam2n3 0 ) ( >= lam2n4 0 ) ( > ( + ( * 1 lam2n0 ) ( * 1 lam2n1 ) ( * Nl1CT1 lam2n2 ) ( * Nl1CT2 lam2n3 ) ( * Nl1CT3 lam2n4 ) ( - 1 ( + Nl1CT2 ( * Nl1x^02 0 ) ) ) ) 0 ) ( = ( + ( * 1 lam2n0 ) ( * Nl1__const_200^01 lam2n2 ) ( * Nl1__const_200^02 lam2n3 ) ( * Nl1__const_200^03 lam2n4 ) ( - ( + 0 Nl1__const_200^02 ) ) ) 0 ) ( = ( + ( * 1 lam2n1 ) ( * Nl1x^01 lam2n2 ) ( * Nl1x^02 lam2n3 ) ( * Nl1x^03 lam2n4 ) ) 0 ) ( = ( + ( * ( - 1 ) lam2n0 ) ( * ( - 1 ) lam2n1 ) ( - ( + 0 ( * Nl1x^02 1 ) ) ) ) 0 ) ) ))
(assert ( or ( and ( >= lam0n0 0 ) ( >= lam0n2 0 ) ( >= lam0n3 0 ) ( >= lam0n4 0 ) ( > ( + ( * 1 lam0n0 ) ( * 1 lam0n1 ) ( * Nl1CT1 lam0n2 ) ( * Nl1CT2 lam0n3 ) ( * Nl1CT3 lam0n4 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * Nl1__const_200^01 lam0n2 ) ( * Nl1__const_200^02 lam0n3 ) ( * Nl1__const_200^03 lam0n4 ) ) 0 ) ( = ( + ( * 1 lam0n1 ) ( * Nl1x^01 lam0n2 ) ( * Nl1x^02 lam0n3 ) ( * Nl1x^03 lam0n4 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * ( - 1 ) lam0n1 ) ) 0 ) ) ( and ( >= lam3n0 0 ) ( >= lam3n2 0 ) ( >= lam3n3 0 ) ( >= lam3n4 0 ) ( > ( + ( * 1 lam3n0 ) ( * 1 lam3n1 ) ( * Nl1CT1 lam3n2 ) ( * Nl1CT2 lam3n3 ) ( * Nl1CT3 lam3n4 ) ( - 1 ( + Nl1CT3 ( * Nl1x^03 0 ) ) ) ) 0 ) ( = ( + ( * 1 lam3n0 ) ( * Nl1__const_200^01 lam3n2 ) ( * Nl1__const_200^02 lam3n3 ) ( * Nl1__const_200^03 lam3n4 ) ( - ( + 0 Nl1__const_200^03 ) ) ) 0 ) ( = ( + ( * 1 lam3n1 ) ( * Nl1x^01 lam3n2 ) ( * Nl1x^02 lam3n3 ) ( * Nl1x^03 lam3n4 ) ) 0 ) ( = ( + ( * ( - 1 ) lam3n0 ) ( * ( - 1 ) lam3n1 ) ( - ( + 0 ( * Nl1x^03 1 ) ) ) ) 0 ) ) ))
(assert ( and ( <= ( + Nl1CT1 ( * ( + 0 Nl1__const_200^01 ) __const_200^0 ) ( * ( + 0 Nl1x^01 ) x^0 ) ) 0 ) ( <= ( + Nl1CT2 ( * ( + 0 Nl1__const_200^02 ) __const_200^0 ) ( * ( + 0 Nl1x^02 ) x^0 ) ) 0 ) ( <= ( + Nl1CT3 ( * ( + 0 Nl1__const_200^03 ) __const_200^0 ) ( * ( + 0 Nl1x^03 ) x^0 ) ) 0 ) ))
(assert ( or ( and ( and ( >= lam10n0 0 ) ( >= lam10n2 0 ) ( >= lam10n3 0 ) ( >= lam10n4 0 ) ( > ( + ( * 1 lam10n0 ) ( * 1 lam10n1 ) ( * Nl1CT1 lam10n2 ) ( * Nl1CT2 lam10n3 ) ( * Nl1CT3 lam10n4 ) ( - 1 ( - ( + RFN1_CT ( * RFN1_x^0 0 ) ) RFN1_CT ) ) ) 0 ) ( = ( + ( * 1 lam10n0 ) ( * Nl1__const_200^01 lam10n2 ) ( * Nl1__const_200^02 lam10n3 ) ( * Nl1__const_200^03 lam10n4 ) ( - ( - ( + 0 RFN1___const_200^0 ) RFN1___const_200^0 ) ) ) 0 ) ( = ( + ( * 1 lam10n1 ) ( * Nl1x^01 lam10n2 ) ( * Nl1x^02 lam10n3 ) ( * Nl1x^03 lam10n4 ) ( - ( - RFN1_x^0 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam10n0 ) ( * ( - 1 ) lam10n1 ) ( - ( + 0 ( * RFN1_x^0 1 ) ) ) ) 0 ) ) ( and ( and ( >= lam8n0 0 ) ( >= lam8n2 0 ) ( >= lam8n3 0 ) ( >= lam8n4 0 ) ( > ( + ( * 1 lam8n0 ) ( * 1 lam8n1 ) ( * Nl1CT1 lam8n2 ) ( * Nl1CT2 lam8n3 ) ( * Nl1CT3 lam8n4 ) ( - 1 ( - RFN1_CT ) ) ) 0 ) ( = ( + ( * 1 lam8n0 ) ( * Nl1__const_200^01 lam8n2 ) ( * Nl1__const_200^02 lam8n3 ) ( * Nl1__const_200^03 lam8n4 ) ( - ( - RFN1___const_200^0 ) ) ) 0 ) ( = ( + ( * 1 lam8n1 ) ( * Nl1x^01 lam8n2 ) ( * Nl1x^02 lam8n3 ) ( * Nl1x^03 lam8n4 ) ( - ( - RFN1_x^0 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam8n0 ) ( * ( - 1 ) lam8n1 ) ) 0 ) ) ( and ( >= lam9n0 0 ) ( >= lam9n2 0 ) ( >= lam9n3 0 ) ( >= lam9n4 0 ) ( > ( + ( * 1 lam9n0 ) ( * 1 lam9n1 ) ( * Nl1CT1 lam9n2 ) ( * Nl1CT2 lam9n3 ) ( * Nl1CT3 lam9n4 ) ( - 1 ( + ( - ( + RFN1_CT ( * RFN1_x^0 0 ) ) RFN1_CT ) 1 ) ) ) 0 ) ( = ( + ( * 1 lam9n0 ) ( * Nl1__const_200^01 lam9n2 ) ( * Nl1__const_200^02 lam9n3 ) ( * Nl1__const_200^03 lam9n4 ) ( - ( - ( + 0 RFN1___const_200^0 ) RFN1___const_200^0 ) ) ) 0 ) ( = ( + ( * 1 lam9n1 ) ( * Nl1x^01 lam9n2 ) ( * Nl1x^02 lam9n3 ) ( * Nl1x^03 lam9n4 ) ( - ( - RFN1_x^0 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam9n0 ) ( * ( - 1 ) lam9n1 ) ( - ( + 0 ( * RFN1_x^0 1 ) ) ) ) 0 ) ) ) ) ( and ( >= lam7n0 0 ) ( >= lam7n2 0 ) ( >= lam7n3 0 ) ( >= lam7n4 0 ) ( > ( + ( * 1 lam7n0 ) ( * 1 lam7n1 ) ( * Nl1CT1 lam7n2 ) ( * Nl1CT2 lam7n3 ) ( * Nl1CT3 lam7n4 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam7n0 ) ( * Nl1__const_200^01 lam7n2 ) ( * Nl1__const_200^02 lam7n3 ) ( * Nl1__const_200^03 lam7n4 ) ) 0 ) ( = ( + ( * 1 lam7n1 ) ( * Nl1x^01 lam7n2 ) ( * Nl1x^02 lam7n3 ) ( * Nl1x^03 lam7n4 ) ) 0 ) ( = ( + ( * ( - 1 ) lam7n0 ) ( * ( - 1 ) lam7n1 ) ) 0 ) ) ))
(check-sat)
(exit)
UnitTests/sat/QF_NIA/From_T2__ex36.t2__p26546_safety_0.smt2 deleted 100644 → 0
+ 0
− 84
View file @ e1544d8e
(set-info :smt-lib-version 2.6)
(set-logic QF_NIA)
(set-info :source |
Generated by: Cristina Borralleras, Daniel Larraz, Albert Oliveras, Enric Rodriguez-Carbonell, Albert Rubio
Generated on: 2017-04-27
Generator: VeryMax
Application: Termination proving
Target solver: barcelogic
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status sat)
(declare-fun Nl37__const_1132^01 () Int)
(declare-fun Nl37__const_15^01 () Int)
(declare-fun Nl37__const_1872^01 () Int)
(declare-fun Nl37cmd1^01 () Int)
(declare-fun Nl37cmd2^01 () Int)
(declare-fun Nl37i16^01 () Int)
(declare-fun Nl37zer^01 () Int)
(declare-fun Nl37__const_1132^02 () Int)
(declare-fun Nl37__const_15^02 () Int)
(declare-fun Nl37__const_1872^02 () Int)
(declare-fun Nl37cmd1^02 () Int)
(declare-fun Nl37cmd2^02 () Int)
(declare-fun Nl37i16^02 () Int)
(declare-fun Nl37zer^02 () Int)
(declare-fun lam0n0 () Int)
(declare-fun lam0n1 () Int)
(declare-fun lam0n2 () Int)
(declare-fun lam0n3 () Int)
(declare-fun lam0n4 () Int)
(declare-fun lam0n5 () Int)
(declare-fun Nl37CT1 () Int)
(declare-fun Nl37CT2 () Int)
(declare-fun lam1n0 () Int)
(declare-fun lam1n1 () Int)
(declare-fun lam1n2 () Int)
(declare-fun lam1n3 () Int)
(declare-fun lam1n4 () Int)
(declare-fun lam1n5 () Int)
(declare-fun lam2n0 () Int)
(declare-fun lam2n1 () Int)
(declare-fun lam2n2 () Int)
(declare-fun lam2n3 () Int)
(declare-fun lam2n4 () Int)
(declare-fun lam2n5 () Int)
(declare-fun lam3n0 () Int)
(declare-fun lam3n1 () Int)
(declare-fun lam3n2 () Int)
(declare-fun lam3n3 () Int)
(declare-fun lam4n0 () Int)
(declare-fun lam4n1 () Int)
(declare-fun lam4n2 () Int)
(declare-fun lam4n3 () Int)
(declare-fun __const_1132^0 () Int)
(declare-fun __const_1872^0 () Int)
(declare-fun zer^0 () Int)
(declare-fun undef2038 () Int)
(declare-fun __const_15^0 () Int)
(declare-fun cmd2^0 () Int)
(declare-fun i16^0 () Int)
(declare-fun undef12771 () Int)
(declare-fun cmd1^0 () Int)
(declare-fun lam5n0 () Int)
(declare-fun lam5n1 () Int)
(declare-fun lam5n2 () Int)
(declare-fun lam5n3 () Int)
(declare-fun lam5n5 () Int)
(declare-fun lam5n6 () Int)
(declare-fun lam5n4 () Int)
(declare-fun lam6n0 () Int)
(declare-fun lam6n1 () Int)
(declare-fun lam6n2 () Int)
(declare-fun lam6n3 () Int)
(declare-fun lam6n5 () Int)
(declare-fun lam6n6 () Int)
(declare-fun lam6n4 () Int)
(assert ( and ( <= ( - 1 ) Nl37__const_1132^01 ) ( <= Nl37__const_1132^01 1 ) ( <= ( - 1 ) Nl37__const_15^01 ) ( <= Nl37__const_15^01 1 ) ( <= ( - 1 ) Nl37__const_1872^01 ) ( <= Nl37__const_1872^01 1 ) ( <= ( - 1 ) Nl37cmd1^01 ) ( <= Nl37cmd1^01 1 ) ( <= ( - 1 ) Nl37cmd2^01 ) ( <= Nl37cmd2^01 1 ) ( <= ( - 1 ) Nl37i16^01 ) ( <= Nl37i16^01 1 ) ( <= ( - 1 ) Nl37zer^01 ) ( <= Nl37zer^01 1 ) ( <= ( - 1 ) Nl37__const_1132^02 ) ( <= Nl37__const_1132^02 1 ) ( <= ( - 1 ) Nl37__const_15^02 ) ( <= Nl37__const_15^02 1 ) ( <= ( - 1 ) Nl37__const_1872^02 ) ( <= Nl37__const_1872^02 1 ) ( <= ( - 1 ) Nl37cmd1^02 ) ( <= Nl37cmd1^02 1 ) ( <= ( - 1 ) Nl37cmd2^02 ) ( <= Nl37cmd2^02 1 ) ( <= ( - 1 ) Nl37i16^02 ) ( <= Nl37i16^02 1 ) ( <= ( - 1 ) Nl37zer^02 ) ( <= Nl37zer^02 1 ) ))
(assert ( or ( and ( >= lam0n0 0 ) ( >= lam0n1 0 ) ( >= lam0n2 0 ) ( >= lam0n3 0 ) ( >= lam0n4 0 ) ( >= lam0n5 0 ) ( > ( + ( * Nl37CT1 lam0n4 ) ( * Nl37CT2 lam0n5 ) ( - 1 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * ( - 1 ) lam0n1 ) ( * Nl37__const_1132^01 lam0n4 ) ( * Nl37__const_1132^02 lam0n5 ) ) 0 ) ( = ( + ( * 1 lam0n2 ) ( * Nl37__const_15^01 lam0n4 ) ( * Nl37__const_15^02 lam0n5 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * 1 lam0n1 ) ( * Nl37__const_1872^01 lam0n4 ) ( * Nl37__const_1872^02 lam0n5 ) ) 0 ) ( = ( + ( * Nl37cmd1^01 lam0n4 ) ( * Nl37cmd1^02 lam0n5 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n2 ) ( * Nl37cmd2^01 lam0n4 ) ( * Nl37cmd2^02 lam0n5 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n3 ) ( * Nl37i16^01 lam0n4 ) ( * Nl37i16^02 lam0n5 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * 1 lam0n1 ) ( * 1 lam0n2 ) ( * Nl37zer^01 lam0n4 ) ( * Nl37zer^02 lam0n5 ) ) 0 ) ( = ( * ( - 1 ) lam0n1 ) 0 ) ) ( and ( >= lam1n0 0 ) ( >= lam1n1 0 ) ( >= lam1n2 0 ) ( >= lam1n3 0 ) ( >= lam1n4 0 ) ( >= lam1n5 0 ) ( > ( + ( * Nl37CT1 lam1n4 ) ( * Nl37CT2 lam1n5 ) ( - 1 ( + Nl37CT1 ( * Nl37i16^01 ( - 1 ) ) ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam1n0 ) ( * ( - 1 ) lam1n1 ) ( * Nl37__const_1132^01 lam1n4 ) ( * Nl37__const_1132^02 lam1n5 ) ( - ( + 0 Nl37__const_1132^01 ) ) ) 0 ) ( = ( + ( * 1 lam1n2 ) ( * Nl37__const_15^01 lam1n4 ) ( * Nl37__const_15^02 lam1n5 ) ( - ( + 0 Nl37__const_15^01 ) ) ) 0 ) ( = ( + ( * 1 lam1n0 ) ( * 1 lam1n1 ) ( * Nl37__const_1872^01 lam1n4 ) ( * Nl37__const_1872^02 lam1n5 ) ( - ( + 0 Nl37__const_1872^01 ) ) ) 0 ) ( = ( + ( * Nl37cmd1^01 lam1n4 ) ( * Nl37cmd1^02 lam1n5 ) ( - ( + 0 Nl37cmd1^01 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam1n2 ) ( * Nl37cmd2^01 lam1n4 ) ( * Nl37cmd2^02 lam1n5 ) ( - ( + 0 Nl37cmd2^01 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam1n3 ) ( * Nl37i16^01 lam1n4 ) ( * Nl37i16^02 lam1n5 ) ( - ( + 0 ( * Nl37i16^01 1 ) ) ) ) 0 ) ( = ( + ( * 1 lam1n0 ) ( * 1 lam1n1 ) ( * 1 lam1n2 ) ( * Nl37zer^01 lam1n4 ) ( * Nl37zer^02 lam1n5 ) ( - ( + 0 Nl37zer^01 ) ) ) 0 ) ( = ( * ( - 1 ) lam1n1 ) 0 ) ) ))
(assert ( or ( and ( >= lam0n0 0 ) ( >= lam0n1 0 ) ( >= lam0n2 0 ) ( >= lam0n3 0 ) ( >= lam0n4 0 ) ( >= lam0n5 0 ) ( > ( + ( * Nl37CT1 lam0n4 ) ( * Nl37CT2 lam0n5 ) ( - 1 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * ( - 1 ) lam0n1 ) ( * Nl37__const_1132^01 lam0n4 ) ( * Nl37__const_1132^02 lam0n5 ) ) 0 ) ( = ( + ( * 1 lam0n2 ) ( * Nl37__const_15^01 lam0n4 ) ( * Nl37__const_15^02 lam0n5 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * 1 lam0n1 ) ( * Nl37__const_1872^01 lam0n4 ) ( * Nl37__const_1872^02 lam0n5 ) ) 0 ) ( = ( + ( * Nl37cmd1^01 lam0n4 ) ( * Nl37cmd1^02 lam0n5 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n2 ) ( * Nl37cmd2^01 lam0n4 ) ( * Nl37cmd2^02 lam0n5 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n3 ) ( * Nl37i16^01 lam0n4 ) ( * Nl37i16^02 lam0n5 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * 1 lam0n1 ) ( * 1 lam0n2 ) ( * Nl37zer^01 lam0n4 ) ( * Nl37zer^02 lam0n5 ) ) 0 ) ( = ( * ( - 1 ) lam0n1 ) 0 ) ) ( and ( >= lam2n0 0 ) ( >= lam2n1 0 ) ( >= lam2n2 0 ) ( >= lam2n3 0 ) ( >= lam2n4 0 ) ( >= lam2n5 0 ) ( > ( + ( * Nl37CT1 lam2n4 ) ( * Nl37CT2 lam2n5 ) ( - 1 ( + Nl37CT2 ( * Nl37i16^02 ( - 1 ) ) ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam2n0 ) ( * ( - 1 ) lam2n1 ) ( * Nl37__const_1132^01 lam2n4 ) ( * Nl37__const_1132^02 lam2n5 ) ( - ( + 0 Nl37__const_1132^02 ) ) ) 0 ) ( = ( + ( * 1 lam2n2 ) ( * Nl37__const_15^01 lam2n4 ) ( * Nl37__const_15^02 lam2n5 ) ( - ( + 0 Nl37__const_15^02 ) ) ) 0 ) ( = ( + ( * 1 lam2n0 ) ( * 1 lam2n1 ) ( * Nl37__const_1872^01 lam2n4 ) ( * Nl37__const_1872^02 lam2n5 ) ( - ( + 0 Nl37__const_1872^02 ) ) ) 0 ) ( = ( + ( * Nl37cmd1^01 lam2n4 ) ( * Nl37cmd1^02 lam2n5 ) ( - ( + 0 Nl37cmd1^02 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam2n2 ) ( * Nl37cmd2^01 lam2n4 ) ( * Nl37cmd2^02 lam2n5 ) ( - ( + 0 Nl37cmd2^02 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam2n3 ) ( * Nl37i16^01 lam2n4 ) ( * Nl37i16^02 lam2n5 ) ( - ( + 0 ( * Nl37i16^02 1 ) ) ) ) 0 ) ( = ( + ( * 1 lam2n0 ) ( * 1 lam2n1 ) ( * 1 lam2n2 ) ( * Nl37zer^01 lam2n4 ) ( * Nl37zer^02 lam2n5 ) ( - ( + 0 Nl37zer^02 ) ) ) 0 ) ( = ( * ( - 1 ) lam2n1 ) 0 ) ) ))
(assert ( and ( not ( <= ( + 1 __const_1132^0 ( * ( - 1 ) __const_1872^0 ) ( * ( - 1 ) zer^0 ) ) 0 ) ) ( not ( <= ( + 1 __const_1132^0 ( * ( - 1 ) __const_1872^0 ) ( * ( - 1 ) zer^0 ) undef2038 ) 0 ) ) ( <= ( + __const_15^0 ( * ( - 1 ) cmd2^0 ) zer^0 ) 0 ) ( = ( + i16^0 ( * ( - 1 ) undef12771 ) ) 0 ) ( <= ( + Nl37CT1 ( * ( + 0 Nl37__const_1132^01 ) __const_1132^0 ) ( * ( + 0 Nl37__const_15^01 ) __const_15^0 ) ( * ( + 0 Nl37__const_1872^01 ) __const_1872^0 ) ( * ( + 0 Nl37cmd1^01 ) cmd1^0 ) ( * ( + 0 Nl37cmd2^01 ) cmd2^0 ) ( * ( + 0 Nl37i16^01 ) i16^0 ) ( * ( + 0 Nl37zer^01 ) zer^0 ) ) 0 ) ( <= ( + Nl37CT2 ( * ( + 0 Nl37__const_1132^02 ) __const_1132^0 ) ( * ( + 0 Nl37__const_15^02 ) __const_15^0 ) ( * ( + 0 Nl37__const_1872^02 ) __const_1872^0 ) ( * ( + 0 Nl37cmd1^02 ) cmd1^0 ) ( * ( + 0 Nl37cmd2^02 ) cmd2^0 ) ( * ( + 0 Nl37i16^02 ) i16^0 ) ( * ( + 0 Nl37zer^02 ) zer^0 ) ) 0 ) ))
(assert ( or ( or ( and ( >= lam5n0 0 ) ( >= lam5n1 0 ) ( >= lam5n2 0 ) ( >= lam5n3 0 ) ( >= lam5n5 0 ) ( >= lam5n6 0 ) ( > ( + ( * 1 lam5n2 ) ( * 1 lam5n3 ) ( * Nl37CT1 lam5n5 ) ( * Nl37CT2 lam5n6 ) ( - 1 ) ) 0 ) ( = ( + ( * ( - 1 ) lam5n2 ) ( * Nl37__const_1132^01 lam5n5 ) ( * Nl37__const_1132^02 lam5n6 ) ) 0 ) ( = ( + ( * 1 lam5n0 ) ( * Nl37__const_15^01 lam5n5 ) ( * Nl37__const_15^02 lam5n6 ) ) 0 ) ( = ( + ( * 1 lam5n4 ) ( * Nl37__const_1872^01 lam5n5 ) ( * Nl37__const_1872^02 lam5n6 ) ) 0 ) ( = ( + ( * 1 lam5n2 ) ( * ( - 1 ) lam5n4 ) ( * Nl37cmd1^01 lam5n5 ) ( * Nl37cmd1^02 lam5n6 ) ) 0 ) ( = ( + ( * ( - 1 ) lam5n0 ) ( * Nl37cmd2^01 lam5n5 ) ( * Nl37cmd2^02 lam5n6 ) ) 0 ) ( = ( + ( * 1 lam5n3 ) ( * Nl37i16^01 lam5n5 ) ( * Nl37i16^02 lam5n6 ) ) 0 ) ( = ( + ( * 1 lam5n0 ) ( * 1 lam5n1 ) ( * Nl37zer^01 lam5n5 ) ( * Nl37zer^02 lam5n6 ) ) 0 ) ) ( and ( >= lam6n0 0 ) ( >= lam6n1 0 ) ( >= lam6n2 0 ) ( >= lam6n3 0 ) ( >= lam6n5 0 ) ( >= lam6n6 0 ) ( > ( + ( * 1 lam6n2 ) ( * 1 lam6n3 ) ( * Nl37CT1 lam6n5 ) ( * Nl37CT2 lam6n6 ) ) 0 ) ( = ( + ( * ( - 1 ) lam6n2 ) ( * Nl37__const_1132^01 lam6n5 ) ( * Nl37__const_1132^02 lam6n6 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam6n0 ) ( * Nl37__const_15^01 lam6n5 ) ( * Nl37__const_15^02 lam6n6 ) ) 0 ) ( = ( + ( * 1 lam6n4 ) ( * Nl37__const_1872^01 lam6n5 ) ( * Nl37__const_1872^02 lam6n6 ) 1 ) 0 ) ( = ( + ( * 1 lam6n2 ) ( * ( - 1 ) lam6n4 ) ( * Nl37cmd1^01 lam6n5 ) ( * Nl37cmd1^02 lam6n6 ) ) 0 ) ( = ( + ( * ( - 1 ) lam6n0 ) ( * Nl37cmd2^01 lam6n5 ) ( * Nl37cmd2^02 lam6n6 ) ) 0 ) ( = ( + ( * 1 lam6n3 ) ( * Nl37i16^01 lam6n5 ) ( * Nl37i16^02 lam6n6 ) ) 0 ) ( = ( + ( * 1 lam6n0 ) ( * 1 lam6n1 ) ( * Nl37zer^01 lam6n5 ) ( * Nl37zer^02 lam6n6 ) 1 ) 0 ) ( = ( - 1 ) 0 ) ) ) ( and ( and ( and ( >= lam3n0 0 ) ( >= lam3n1 0 ) ( >= lam3n2 0 ) ( > ( - 1 Nl37CT1 ) 0 ) ( = ( + ( * ( - 1 ) lam3n0 ) ( * ( - 1 ) lam3n1 ) ( - ( + 0 Nl37__const_1132^01 ) ) ) 0 ) ( = ( + ( * 1 lam3n2 ) ( - ( + 0 Nl37__const_15^01 ) ) ) 0 ) ( = ( + ( * 1 lam3n0 ) ( * 1 lam3n1 ) ( - ( + 0 Nl37__const_1872^01 ) ) ) 0 ) ( = ( - ( + 0 Nl37cmd1^01 ) ) 0 ) ( = ( + ( * ( - 1 ) lam3n2 ) ( - ( + 0 Nl37cmd2^01 ) ) ) 0 ) ( = ( + ( * 1 lam3n3 ) ( - ( + 0 Nl37i16^01 ) ) ) 0 ) ( = ( + ( * 1 lam3n0 ) ( * 1 lam3n1 ) ( * 1 lam3n2 ) ( - ( + 0 Nl37zer^01 ) ) ) 0 ) ( = ( * ( - 1 ) lam3n1 ) 0 ) ( = ( * ( - 1 ) lam3n3 ) 0 ) ) ( and ( >= lam4n0 0 ) ( >= lam4n1 0 ) ( >= lam4n2 0 ) ( > ( - 1 Nl37CT2 ) 0 ) ( = ( + ( * ( - 1 ) lam4n0 ) ( * ( - 1 ) lam4n1 ) ( - ( + 0 Nl37__const_1132^02 ) ) ) 0 ) ( = ( + ( * 1 lam4n2 ) ( - ( + 0 Nl37__const_15^02 ) ) ) 0 ) ( = ( + ( * 1 lam4n0 ) ( * 1 lam4n1 ) ( - ( + 0 Nl37__const_1872^02 ) ) ) 0 ) ( = ( - ( + 0 Nl37cmd1^02 ) ) 0 ) ( = ( + ( * ( - 1 ) lam4n2 ) ( - ( + 0 Nl37cmd2^02 ) ) ) 0 ) ( = ( + ( * 1 lam4n3 ) ( - ( + 0 Nl37i16^02 ) ) ) 0 ) ( = ( + ( * 1 lam4n0 ) ( * 1 lam4n1 ) ( * 1 lam4n2 ) ( - ( + 0 Nl37zer^02 ) ) ) 0 ) ( = ( * ( - 1 ) lam4n1 ) 0 ) ( = ( * ( - 1 ) lam4n3 ) 0 ) ) ) ( and ( >= lam0n0 0 ) ( >= lam0n1 0 ) ( >= lam0n2 0 ) ( >= lam0n3 0 ) ( >= lam0n4 0 ) ( >= lam0n5 0 ) ( > ( + ( * Nl37CT1 lam0n4 ) ( * Nl37CT2 lam0n5 ) ( - 1 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * ( - 1 ) lam0n1 ) ( * Nl37__const_1132^01 lam0n4 ) ( * Nl37__const_1132^02 lam0n5 ) ) 0 ) ( = ( + ( * 1 lam0n2 ) ( * Nl37__const_15^01 lam0n4 ) ( * Nl37__const_15^02 lam0n5 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * 1 lam0n1 ) ( * Nl37__const_1872^01 lam0n4 ) ( * Nl37__const_1872^02 lam0n5 ) ) 0 ) ( = ( + ( * Nl37cmd1^01 lam0n4 ) ( * Nl37cmd1^02 lam0n5 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n2 ) ( * Nl37cmd2^01 lam0n4 ) ( * Nl37cmd2^02 lam0n5 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n3 ) ( * Nl37i16^01 lam0n4 ) ( * Nl37i16^02 lam0n5 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * 1 lam0n1 ) ( * 1 lam0n2 ) ( * Nl37zer^01 lam0n4 ) ( * Nl37zer^02 lam0n5 ) ) 0 ) ( = ( * ( - 1 ) lam0n1 ) 0 ) ) ) ))
(check-sat)
(exit)
UnitTests/sat/QF_NIA/From_T2__small29.t2__p23958_edge_closing_0.smt2 deleted 100644 → 0
+ 0
− 56
View file @ e1544d8e
(set-info :smt-lib-version 2.6)
(set-logic QF_NIA)
(set-info :source |
Generated by: Cristina Borralleras, Daniel Larraz, Albert Oliveras, Enric Rodriguez-Carbonell, Albert Rubio
Generated on: 2017-04-27
Generator: VeryMax
Application: Termination proving
Target solver: barcelogic
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status sat)
(declare-fun Nl1x^01 () Int)
(declare-fun Nl1y^01 () Int)
(declare-fun Nl1x^02 () Int)
(declare-fun Nl1y^02 () Int)
(declare-fun Nl1x^03 () Int)
(declare-fun Nl1y^03 () Int)
(declare-fun lam0n1 () Int)
(declare-fun lam0n2 () Int)
(declare-fun lam0n3 () Int)
(declare-fun Nl1CT1 () Int)
(declare-fun Nl1CT2 () Int)
(declare-fun Nl1CT3 () Int)
(declare-fun lam0n0 () Int)
(declare-fun lam1n1 () Int)
(declare-fun lam1n2 () Int)
(declare-fun lam1n3 () Int)
(declare-fun lam1n0 () Int)
(declare-fun lam2n1 () Int)
(declare-fun lam2n2 () Int)
(declare-fun lam2n3 () Int)
(declare-fun lam2n0 () Int)
(declare-fun lam3n1 () Int)
(declare-fun lam3n2 () Int)
(declare-fun lam3n3 () Int)
(declare-fun lam3n0 () Int)
(declare-fun x^0 () Int)
(declare-fun y^0 () Int)
(declare-fun FV_x^0_1 () Int)
(declare-fun FV_y^0_1 () Int)
(declare-fun lam7n0 () Int)
(declare-fun lam7n1 () Int)
(declare-fun lam7n2 () Int)
(declare-fun lam7n3 () Int)
(declare-fun FV_x^0_2 () Int)
(declare-fun FV_y^0_2 () Int)
(assert ( and ( <= ( - 1 ) Nl1x^01 ) ( <= Nl1x^01 1 ) ( <= ( - 1 ) Nl1y^01 ) ( <= Nl1y^01 1 ) ( <= ( - 1 ) Nl1x^02 ) ( <= Nl1x^02 1 ) ( <= ( - 1 ) Nl1y^02 ) ( <= Nl1y^02 1 ) ( <= ( - 1 ) Nl1x^03 ) ( <= Nl1x^03 1 ) ( <= ( - 1 ) Nl1y^03 ) ( <= Nl1y^03 1 ) ))
(assert ( or ( and ( >= lam0n1 0 ) ( >= lam0n2 0 ) ( >= lam0n3 0 ) ( > ( + ( * Nl1CT1 lam0n1 ) ( * Nl1CT2 lam0n2 ) ( * Nl1CT3 lam0n3 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * Nl1x^01 lam0n1 ) ( * Nl1x^02 lam0n2 ) ( * Nl1x^03 lam0n3 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * Nl1y^01 lam0n1 ) ( * Nl1y^02 lam0n2 ) ( * Nl1y^03 lam0n3 ) ) 0 ) ) ( and ( >= lam1n1 0 ) ( >= lam1n2 0 ) ( >= lam1n3 0 ) ( > ( + ( * Nl1CT1 lam1n1 ) ( * Nl1CT2 lam1n2 ) ( * Nl1CT3 lam1n3 ) ( - 1 Nl1CT1 ) ) 0 ) ( = ( + ( * 1 lam1n0 ) ( * Nl1x^01 lam1n1 ) ( * Nl1x^02 lam1n2 ) ( * Nl1x^03 lam1n3 ) ( - ( + 0 Nl1x^01 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam1n0 ) ( * Nl1y^01 lam1n1 ) ( * Nl1y^02 lam1n2 ) ( * Nl1y^03 lam1n3 ) ( - ( + 0 Nl1y^01 ) ) ) 0 ) ) ))
(assert ( or ( and ( >= lam0n1 0 ) ( >= lam0n2 0 ) ( >= lam0n3 0 ) ( > ( + ( * Nl1CT1 lam0n1 ) ( * Nl1CT2 lam0n2 ) ( * Nl1CT3 lam0n3 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * Nl1x^01 lam0n1 ) ( * Nl1x^02 lam0n2 ) ( * Nl1x^03 lam0n3 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * Nl1y^01 lam0n1 ) ( * Nl1y^02 lam0n2 ) ( * Nl1y^03 lam0n3 ) ) 0 ) ) ( and ( >= lam2n1 0 ) ( >= lam2n2 0 ) ( >= lam2n3 0 ) ( > ( + ( * Nl1CT1 lam2n1 ) ( * Nl1CT2 lam2n2 ) ( * Nl1CT3 lam2n3 ) ( - 1 Nl1CT2 ) ) 0 ) ( = ( + ( * 1 lam2n0 ) ( * Nl1x^01 lam2n1 ) ( * Nl1x^02 lam2n2 ) ( * Nl1x^03 lam2n3 ) ( - ( + 0 Nl1x^02 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam2n0 ) ( * Nl1y^01 lam2n1 ) ( * Nl1y^02 lam2n2 ) ( * Nl1y^03 lam2n3 ) ( - ( + 0 Nl1y^02 ) ) ) 0 ) ) ))
(assert ( or ( and ( >= lam0n1 0 ) ( >= lam0n2 0 ) ( >= lam0n3 0 ) ( > ( + ( * Nl1CT1 lam0n1 ) ( * Nl1CT2 lam0n2 ) ( * Nl1CT3 lam0n3 ) ( - 1 ) ) 0 ) ( = ( + ( * 1 lam0n0 ) ( * Nl1x^01 lam0n1 ) ( * Nl1x^02 lam0n2 ) ( * Nl1x^03 lam0n3 ) ) 0 ) ( = ( + ( * ( - 1 ) lam0n0 ) ( * Nl1y^01 lam0n1 ) ( * Nl1y^02 lam0n2 ) ( * Nl1y^03 lam0n3 ) ) 0 ) ) ( and ( >= lam3n1 0 ) ( >= lam3n2 0 ) ( >= lam3n3 0 ) ( > ( + ( * Nl1CT1 lam3n1 ) ( * Nl1CT2 lam3n2 ) ( * Nl1CT3 lam3n3 ) ( - 1 Nl1CT3 ) ) 0 ) ( = ( + ( * 1 lam3n0 ) ( * Nl1x^01 lam3n1 ) ( * Nl1x^02 lam3n2 ) ( * Nl1x^03 lam3n3 ) ( - ( + 0 Nl1x^03 ) ) ) 0 ) ( = ( + ( * ( - 1 ) lam3n0 ) ( * Nl1y^01 lam3n1 ) ( * Nl1y^02 lam3n2 ) ( * Nl1y^03 lam3n3 ) ( - ( + 0 Nl1y^03 ) ) ) 0 ) ) ))
(assert ( and ( <= ( + Nl1CT1 ( * Nl1x^01 FV_x^0_1 ) ( * Nl1y^01 FV_y^0_1 ) ) 0 ) ( <= ( + Nl1CT2 ( * Nl1x^02 FV_x^0_1 ) ( * Nl1y^02 FV_y^0_1 ) ) 0 ) ( <= ( + Nl1CT3 ( * Nl1x^03 FV_x^0_1 ) ( * Nl1y^03 FV_y^0_1 ) ) 0 ) ( <= ( + ( * ( - 1 ) FV_x^0_1 ) FV_y^0_1 ) 0 ) ))
(assert ( and ( >= lam7n0 0 ) ( >= lam7n1 0 ) ( >= lam7n2 0 ) ( >= lam7n3 0 ) ( > ( + ( * 1 lam7n0 ) ( * Nl1CT1 lam7n1 ) ( * Nl1CT2 lam7n2 ) ( * Nl1CT3 lam7n3 ) ( - 1 ) ) 0 ) ( = ( + ( * ( - 1 ) lam7n0 ) ( * Nl1x^01 lam7n1 ) ( * Nl1x^02 lam7n2 ) ( * Nl1x^03 lam7n3 ) ) 0 ) ( = ( + ( * 1 lam7n0 ) ( * Nl1y^01 lam7n1 ) ( * Nl1y^02 lam7n2 ) ( * Nl1y^03 lam7n3 ) ) 0 ) ))
(assert ( and ( and ( <= ( + Nl1CT1 ( * Nl1x^01 FV_x^0_2 ) ( * Nl1y^01 FV_y^0_2 ) ) 0 ) ( <= ( + Nl1CT2 ( * Nl1x^02 FV_x^0_2 ) ( * Nl1y^02 FV_y^0_2 ) ) 0 ) ( <= ( + Nl1CT3 ( * Nl1x^03 FV_x^0_2 ) ( * Nl1y^03 FV_y^0_2 ) ) 0 ) ) ( = ( + FV_x^0_2 ( * ( - 1 ) FV_y^0_2 ) ) 0 ) ))
(check-sat)
(exit)
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment