}
}
d_addedLemmas += addedLemmas;
- Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << std::endl;
- return true;
+ Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << ", incomplete=" << riter.d_incomplete << std::endl;
+ return addedLemmas>0 || !riter.d_incomplete;
}else{
Trace("fmc-exh") << "----Finished Exhaustive instantiate, failed." << std::endl;
return false;
}else if( n.getKind()==ITE ){
newHasPol = (child!=0) && hasPol;
newPol = pol;
+ }else if( n.getKind()==FORALL ){
+ newHasPol = (child==1) && hasPol;
+ newPol = pol;
}else{
newHasPol = false;
newPol = pol;
void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons,
std::vector< Node >& conj ){
if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){
- Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl;
+ Trace("quantifiers-rewrite-ite-debug") << "Split tester condition : " << n << std::endl;
Node x = n[0][0];
std::map< Node, Node >::iterator itp = pcons.find( x );
if( itp!=pcons.end() ){
return 0;
}
-bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) {
+bool addEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond, bool& conflict ) {
std::map< Node, bool >::iterator it = currCond.find( n );
if( it==currCond.end() ){
- Trace("quantifiers-rewrite-ite-debug") << "ITE cond : " << n << " -> " << pol << std::endl;
+ Trace("quantifiers-rewrite-term-debug") << "cond : " << n << " -> " << pol << std::endl;
new_cond.push_back( n );
currCond[n] = pol;
return true;
}else{
- Assert( it->second==pol );
+ if( it->second!=pol ){
+ Trace("quantifiers-rewrite-term-debug") << "CONFLICTING cond : " << n << " -> " << pol << std::endl;
+ conflict = true;
+ }
return false;
}
}
-void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond ) {
+void setEntailedCond( Node n, bool pol, std::map< Node, bool >& currCond, std::vector< Node >& new_cond, bool& conflict ) {
if( ( n.getKind()==AND && pol ) || ( n.getKind()==OR && !pol ) ){
for( unsigned i=0; i<n.getNumChildren(); i++ ){
- setEntailedCond( n[i], pol, currCond, new_cond );
+ setEntailedCond( n[i], pol, currCond, new_cond, conflict );
+ if( conflict ){
+ break;
+ }
}
}else if( n.getKind()==NOT ){
- setEntailedCond( n[0], !pol, currCond, new_cond );
+ setEntailedCond( n[0], !pol, currCond, new_cond, conflict );
+ return;
}else if( n.getKind()==ITE ){
int pol = getEntailedCond( n, currCond );
if( pol==1 ){
- setEntailedCond( n[1], pol, currCond, new_cond );
+ setEntailedCond( n[1], pol, currCond, new_cond, conflict );
}else if( pol==-1 ){
- setEntailedCond( n[2], pol, currCond, new_cond );
+ setEntailedCond( n[2], pol, currCond, new_cond, conflict );
}
}
- if( addEntailedCond( n, pol, currCond, new_cond ) ){
+ if( addEntailedCond( n, pol, currCond, new_cond, conflict ) ){
if( n.getKind()==APPLY_TESTER ){
const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
unsigned index = Datatype::indexOf(n.getOperator().toExpr());
for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
if( i!=index ){
Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[i].getTester() ), n[0] );
- addEntailedCond( t, false, currCond, new_cond );
+ addEntailedCond( t, false, currCond, new_cond, conflict );
}
}
}else{
if( dt.getNumConstructors()==2 ){
int oindex = 1-index;
Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[oindex].getTester() ), n[0] );
- addEntailedCond( t, true, currCond, new_cond );
+ addEntailedCond( t, true, currCond, new_cond, conflict );
}
}
}
Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond,
std::map< Node, Node >& cache, std::map< Node, Node >& icache,
std::vector< Node >& new_vars, std::vector< Node >& new_conds ) {
+ Trace("quantifiers-rewrite-term-debug2") << "computeProcessTerms " << body << " " << hasPol << " " << pol << std::endl;
Node ret;
std::map< Node, Node >::iterator iti = cache.find( body );
if( iti!=cache.end() ){
ret = iti->second;
+ Trace("quantifiers-rewrite-term-debug2") << "Return (cached) " << ret << " for " << body << std::endl;
}else{
- bool do_ite = false;
- //only do context dependent processing up to ITE depth 8
- if( body.getKind()==ITE && nCurrCond<8 ){
- do_ite = true;
- nCurrCond = nCurrCond + 1;
- }
+ bool firstTimeCD = true;
bool changed = false;
std::vector< Node > children;
for( size_t i=0; i<body.getNumChildren(); i++ ){
std::vector< Node > new_cond;
- if( do_ite && i>0 ){
- setEntailedCond( children[0], i==1, currCond, new_cond );
- cache.clear();
+ bool conflict = false;
+ //only do context dependent processing up to depth 8
+ if( nCurrCond<8 ){
+ if( firstTimeCD ){
+ firstTimeCD = false;
+ nCurrCond = nCurrCond + 1;
+ }
+ if( Trace.isOn("quantifiers-rewrite-term-debug") ){
+ //if( ( body.getKind()==ITE && i>0 ) || ( hasPol && ( ( body.getKind()==OR && pol ) || (body.getKind()==AND && !pol ) ) ) ){
+ if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){
+ Trace("quantifiers-rewrite-term-debug") << "---rewrite " << body[i] << " under conditions:----" << std::endl;
+ }
+ }
+ if( body.getKind()==ITE && i>0 ){
+ setEntailedCond( children[0], i==1, currCond, new_cond, conflict );
+ //should not conflict (entailment check failed)
+ Assert( !conflict );
+ }
+ //if( hasPol && ( ( body.getKind()==OR && pol ) || ( body.getKind()==AND && !pol ) ) ){
+ // bool use_pol = !pol;
+ if( body.getKind()==OR || body.getKind()==AND ){
+ bool use_pol = body.getKind()==AND;
+ for( unsigned j=0; j<body.getNumChildren(); j++ ){
+ if( j<i ){
+ setEntailedCond( children[j], use_pol, currCond, new_cond, conflict );
+ }else if( j>i ){
+ setEntailedCond( body[j], use_pol, currCond, new_cond, conflict );
+ }
+ }
+ if( conflict ){
+ Trace("quantifiers-rewrite-term-debug") << "-------conflict, return " << !use_pol << std::endl;
+ ret = NodeManager::currentNM()->mkConst( !use_pol );
+ }
+ }
+ if( !new_cond.empty() ){
+ cache.clear();
+ }
+ if( Trace.isOn("quantifiers-rewrite-term-debug") ){
+ //if( ( body.getKind()==ITE && i>0 ) || ( hasPol && ( ( body.getKind()==OR && pol ) || (body.getKind()==AND && !pol ) ) ) ){
+ if( ( body.getKind()==ITE && i>0 ) || body.getKind()==OR || body.getKind()==AND ){
+ Trace("quantifiers-rewrite-term-debug") << "-------" << std::endl;
+ }
+ }
}
- bool newHasPol;
- bool newPol;
- QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
- Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
- if( body.getKind()==ITE ){
- if( i==0 ){
+ if( !conflict ){
+ bool newHasPol;
+ bool newPol;
+ QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
+ Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
+ if( body.getKind()==ITE && i==0 ){
int res = getEntailedCond( nn, currCond );
+ Trace("quantifiers-rewrite-term-debug") << "Condition for " << body << " is " << nn << ", entailment check=" << res << std::endl;
if( res==1 ){
ret = computeProcessTerms2( body[1], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
- break;
}else if( res==-1 ){
ret = computeProcessTerms2( body[2], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
- break;
- }
- }else{
- if( !new_cond.empty() ){
- for( unsigned j=0; j<new_cond.size(); j++ ){
- currCond.erase( new_cond[j] );
- }
- cache.clear();
}
}
+ children.push_back( nn );
+ changed = changed || nn!=body[i];
+ }
+ if( !new_cond.empty() ){
+ for( unsigned j=0; j<new_cond.size(); j++ ){
+ currCond.erase( new_cond[j] );
+ }
+ cache.clear();
+ }
+ if( !ret.isNull() ){
+ break;
}
- children.push_back( nn );
- changed = changed || nn!=body[i];
}
- if( ret.isNull() && changed ){
- if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
- children.insert( children.begin(), body.getOperator() );
+ if( ret.isNull() ){
+ if( changed ){
+ if( body.getMetaKind() == kind::metakind::PARAMETERIZED ){
+ children.insert( children.begin(), body.getOperator() );
+ }
+ ret = NodeManager::currentNM()->mkNode( body.getKind(), children );
+ }else{
+ ret = body;
}
- ret = NodeManager::currentNM()->mkNode( body.getKind(), children );
- }else{
- ret = body;
}
+ Trace("quantifiers-rewrite-term-debug2") << "Returning " << ret << " for " << body << std::endl;
cache[body] = ret;
}
ext-ex-deq-trigger.smt2 \
matching-lia-1arg.smt2 \
RND_4_16.smt2 \
- cdt-0208-to.smt2
+ cdt-0208-to.smt2 \
+ psyco-196.smt2 \
+ agg-rew-test.smt2 \
+ agg-rew-test-cf.smt2 \
+ rew-to-0211-dd.smt2 \
+ rew-to-scala.smt2
# regression can be solved with --finite-model-find --fmf-inst-engine
--- /dev/null
+(set-logic UFLIA)
+(set-info :status sat)
+(declare-fun Q (Int Int) Bool)
+(assert (forall ((x Int)) (or (and (or (Q 0 x) (Q 1 x)) (Q 2 x)) (not (Q 2 x)) (not (Q 1 x)))))
+(check-sat)
--- /dev/null
+(set-logic UFLIA)
+(set-info :status sat)
+(declare-fun Q (Int Int) Bool)
+(assert (forall ((x Int)) (=> (Q 0 x) (or (ite (Q 0 x) (not (Q 2 x)) (Q 3 x)) (Q 2 x)))))
+(check-sat)
--- /dev/null
+(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)
+
--- /dev/null
+(set-logic UFLIA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun boolIff (Int Int) Int)
+(declare-fun PeerGroupPlaceholder_ () Int)
+(declare-fun intGreater (Int Int) Int)
+(declare-fun IfThenElse_ (Int Int Int) Int)
+(declare-fun System.IConvertible () Int)
+(declare-fun CONCVARSYM (Int) Int)
+(declare-fun throwException_in () Int)
+(declare-fun SharingMode_Unshared_ () Int)
+(declare-fun System.Reflection.IReflect () Int)
+(declare-fun result_0_ () Int)
+(declare-fun block3502_2_block3553_correct () Int)
+(declare-fun int_m2147483648 () Int)
+(declare-fun local0_0 () Int)
+(declare-fun System.Int32 () Int)
+(declare-fun local0_1 () Int)
+(declare-fun block3536_2_block3553_correct () Int)
+(declare-fun block3553_correct () Int)
+(declare-fun intAtMost (Int Int) Int)
+(declare-fun multiply (Int Int) Int)
+(declare-fun Is_ (Int Int) Int)
+(declare-fun Smt.true () Int)
+(declare-fun ElementType_ (Int) Int)
+(declare-fun divide (Int Int) Int)
+(declare-fun int_m9223372036854775808 () Int)
+(declare-fun divides (Int Int) Int)
+(declare-fun stack0b_0 () Int)
+(declare-fun select1 (Int Int) Int)
+(declare-fun stack0b_1 () Int)
+(declare-fun store1 (Int Int Int) Int)
+(declare-fun select2 (Int Int Int) Int)
+(declare-fun nullObject () Int)
+(declare-fun store2 (Int Int Int Int) Int)
+(declare-fun false3451to3468_correct () Int)
+(declare-fun modulo (Int Int) Int)
+(declare-fun System.IComparable () Int)
+(declare-fun ownerRef_ () Int)
+(declare-fun StructSet_ (Int Int Int) Int)
+(declare-fun AsDirectSubClass (Int Int) Int)
+(declare-fun System.IEquatable_1...System.String () Int)
+(declare-fun System.Boolean () Int)
+(declare-fun shl_ (Int Int) Int)
+(declare-fun DimLength_ (Int Int) Int)
+(declare-fun anyEqual (Int Int) Int)
+(declare-fun System.Array () Int)
+(declare-fun block3451_correct () Int)
+(declare-fun System.Collections.Generic.IEnumerable_1...System.Char () Int)
+(declare-fun System.Reflection.ICustomAttributeProvider () Int)
+(declare-fun SharingMode_LockProtected_ () Int)
+(declare-fun IsMemberlessType_ (Int) Int)
+(declare-fun PartOfLine () Int)
+(declare-fun System.UInt16 () Int)
+(declare-fun false3434to3451_correct () Int)
+(declare-fun ClassRepr (Int) Int)
+(declare-fun System.Runtime.InteropServices._Type () Int)
+(declare-fun boolNot (Int) Int)
+(declare-fun Microsoft.Contracts.ICheckedException () Int)
+(declare-fun System.Exception () Int)
+(declare-fun System.Runtime.InteropServices._MemberInfo () Int)
+(declare-fun boolAnd (Int Int) Int)
+(declare-fun boolImplies (Int Int) Int)
+(declare-fun Unbox (Int) Int)
+(declare-fun intAtLeast (Int Int) Int)
+(declare-fun ownerFrame_ () Int)
+(declare-fun int_4294967295 () Int)
+(declare-fun IsAllocated (Int Int) Int)
+(declare-fun TypeName (Int) Int)
+(declare-fun AsPeerField (Int) Int)
+(declare-fun int_9223372036854775807 () Int)
+(declare-fun AsRepField (Int Int) Int)
+(declare-fun System.Reflection.MemberInfo () Int)
+(declare-fun ArrayCategoryValue_ () Int)
+(declare-fun is (Int Int) Int)
+(declare-fun Microsoft.Contracts.GuardException () Int)
+(declare-fun InRange (Int Int) Bool)
+(declare-fun AsOwner (Int Int) Int)
+(declare-fun System.Int64 () Int)
+(declare-fun System.Runtime.InteropServices._Exception () Int)
+(declare-fun or_ (Int Int) Int)
+(declare-fun As_ (Int Int) Int)
+(declare-fun exposeVersion_ () Int)
+(declare-fun true3434to3536_correct () Int)
+(declare-fun System.Type () Int)
+(declare-fun intLess (Int Int) Int)
+(declare-fun AsImmutable_ (Int) Int)
+(declare-fun NonNullFieldsAreInitialized_ () Int)
+(declare-fun block3417_correct () Int)
+(declare-fun LBound_ (Int Int) Int)
+(declare-fun System.Object () Int)
+(declare-fun System.UInt32 () Int)
+(declare-fun localinv_ () Int)
+(declare-fun inv_ () Int)
+(declare-fun Interval () Int)
+(declare-fun stack50000o_0 () Int)
+(declare-fun stack50000o_1 () Int)
+(declare-fun Heap_0_ () Int)
+(declare-fun entry_correct () Int)
+(declare-fun FirstConsistentOwner_ () Int)
+(declare-fun UnboxedType (Int) Int)
+(declare-fun AsRefField (Int Int) Int)
+(declare-fun System.Byte () Int)
+(declare-fun this () Int)
+(declare-fun stack1o_0 () Int)
+(declare-fun int_2147483647 () Int)
+(declare-fun ArrayCategoryRef_ () Int)
+(declare-fun Interval.a () Int)
+(declare-fun Interval.b () Int)
+(declare-fun stack1i_0 () Int)
+(declare-fun Heap_ () Int)
+(declare-fun Length_ (Int) Int)
+(declare-fun System.Runtime.Serialization.ISerializable () Int)
+(declare-fun AsNonNullRefField (Int Int) Int)
+(declare-fun IsHeap (Int) Int)
+(declare-fun Heap_1_ () Int)
+(declare-fun UBound_ (Int Int) Int)
+(declare-fun Cell () Int)
+(declare-fun System.String () Int)
+(declare-fun System.String.IsInterned_System.String_notnull_ (Int) Int)
+(declare-fun Rank_ (Int) Int)
+(declare-fun UnknownRef_ () Int)
+(declare-fun RefArraySet (Int Int Int) Int)
+(declare-fun ValueArraySet (Int Int Int) Int)
+(declare-fun stack50000o () Int)
+(declare-fun boolOr (Int Int) Int)
+(declare-fun sharingMode_ () Int)
+(declare-fun subtypes (Int Int) Bool)
+(declare-fun System.IComparable_1...System.String () Int)
+(declare-fun System.String.Equals_System.String_System.String_ (Int Int) Int)
+(declare-fun block3434_correct () Int)
+(declare-fun anyNeq (Int Int) Int)
+(declare-fun IsStaticField (Int) Int)
+(declare-fun SS_Display.Return.Local_0 () Int)
+(declare-fun IsNotNull_ (Int Int) Int)
+(declare-fun typeof_ (Int) Int)
+(declare-fun ArrayCategoryNonNullRef_ () Int)
+(declare-fun RefArrayGet (Int Int) Int)
+(declare-fun ValueArrayGet (Int Int) Int)
+(declare-fun TypeObject (Int) Int)
+(declare-fun and_ (Int Int) Int)
+(declare-fun BoxTester (Int Int) Int)
+(declare-fun Microsoft.Contracts.ObjectInvariantException () Int)
+(declare-fun block3468_correct () Int)
+(declare-fun IsValueType_ (Int) Int)
+(declare-fun Heap_2_ () Int)
+(declare-fun AsRangeField (Int Int) Int)
+(declare-fun System.SByte () Int)
+(declare-fun BeingConstructed_ () Int)
+(declare-fun block3502_correct () Int)
+(declare-fun FieldDependsOnFCO_ (Int Int Int) Int)
+(declare-fun NonNullRefArray (Int Int) Int)
+(declare-fun RefArray (Int Int) Int)
+(declare-fun ArrayCategory_ (Int) Int)
+(declare-fun stack0b () Int)
+(declare-fun Cell.Value () Int)
+(declare-fun AsPureObject_ (Int) Int)
+(declare-fun System.String.Equals_System.String_ (Int Int) Int)
+(declare-fun System.Int16 () Int)
+(declare-fun block3536_correct () Int)
+(declare-fun AsMutable_ (Int) Int)
+(declare-fun System.Char () Int)
+(declare-fun System.UInt64 () Int)
+(declare-fun StructGet_ (Int Int) Int)
+(declare-fun OneClassDown (Int Int) Int)
+(declare-fun ArrayIndex (Int Int Int Int) Int)
+(declare-fun stack0o_0 () Int)
+(declare-fun Box (Int Int) Int)
+(declare-fun stack0o_1 () Int)
+(declare-fun int_18446744073709551615 () Int)
+(declare-fun shr_ (Int Int) Int)
+(declare-fun stack0i_0 () Int)
+(declare-fun block3553_2_GeneratedUnifiedExit_correct () Int)
+(declare-fun System.ICloneable () Int)
+(declare-fun IsDirectlyModifiableField (Int) Int)
+(declare-fun StringLength_ (Int) Int)
+(declare-fun allocated_ () Int)
+(declare-fun BaseClass_ (Int) Int)
+(declare-fun ValueArray (Int Int) Int)
+(declare-fun Smt.false () Int)
+(declare-fun true3451to3502_correct () Int)
+(declare-fun IsImmutable_ (Int) Int)
+(declare-fun elements_ () Int)
+(declare-fun DeclType (Int) Int)
+(declare-fun System.Collections.IEnumerable () Int)
+(declare-fun ReallyLastGeneratedExit_correct () Int)
+(assert (forall ((?o Int) (?T Int)) (! (= (= (IsNotNull_ ?o ?T) Smt.true) (and (not (= ?o nullObject)) (= (Is_ ?o ?T) Smt.true))) :pattern ((IsNotNull_ ?o ?T)) )))
+(assert (forall ((?h Int) (?o Int) (?f Int) (?T Int)) (! (=> (and (= (IsHeap ?h) Smt.true) (not (= ?o nullObject)) (or (not (= ?o BeingConstructed_)) (= (= (select2 ?h BeingConstructed_ NonNullFieldsAreInitialized_) Smt.true) true))) (not (= (select2 ?h ?o (AsNonNullRefField ?f ?T)) nullObject))) :pattern ((select2 ?h ?o (AsNonNullRefField ?f ?T))) )))
+(assert (forall ((?o Int) (?T Int)) (! (=> (and (not (= ?o nullObject)) (not (= ?o BeingConstructed_)) (subtypes (typeof_ ?o) (AsImmutable_ ?T))) (forall ((?h Int)) (! (let ((?v_0 (typeof_ ?o))) (=> (= (IsHeap ?h) Smt.true) (and (= (select2 ?h ?o inv_) ?v_0) (= (select2 ?h ?o localinv_) ?v_0) (= (select2 ?h ?o ownerFrame_) PeerGroupPlaceholder_) (= (AsOwner ?o (select2 ?h ?o ownerRef_)) ?o) (forall ((?t Int)) (! (=> (= (AsOwner ?o (select2 ?h ?t ownerRef_)) ?o) (or (= ?t ?o) (not (= (select2 ?h ?t ownerFrame_) PeerGroupPlaceholder_)))) :pattern ((AsOwner ?o (select2 ?h ?t ownerRef_))) ))))) :pattern ((IsHeap ?h)) ))) :pattern ((subtypes (typeof_ ?o) (AsImmutable_ ?T))) )))
+(assert (= (IsValueType_ System.SByte) Smt.true))
+(assert (= (IsValueType_ System.Byte) Smt.true))
+(assert (= (IsValueType_ System.Int16) Smt.true))
+(assert (= (IsValueType_ System.UInt16) Smt.true))
+(assert (= (IsValueType_ System.Int32) Smt.true))
+(assert (= (IsValueType_ System.UInt32) Smt.true))
+(assert (= (IsValueType_ System.Int64) Smt.true))
+(assert (= (IsValueType_ System.UInt64) Smt.true))
+(assert (= (IsValueType_ System.Char) Smt.true))
+(assert (< int_m9223372036854775808 int_m2147483648))
+(assert (< int_m2147483648 (- 0 100000)))
+(assert (< 100000 int_2147483647))
+(assert (< int_2147483647 int_4294967295))
+(assert (< int_4294967295 int_9223372036854775807))
+(assert (< int_9223372036854775807 int_18446744073709551615))
+(assert (not (= (IsStaticField Cell.Value) Smt.true)))
+(assert (= (IsDirectlyModifiableField Cell.Value) Smt.true))
+(assert (= (DeclType Cell.Value) Cell))
+(assert (= (AsRangeField Cell.Value System.Int32) Cell.Value))
+(assert (not (= (IsStaticField Interval.a) Smt.true)))
+(assert (= (IsDirectlyModifiableField Interval.a) Smt.true))
+(assert (= (AsRepField Interval.a Interval) Interval.a))
+(assert (= (DeclType Interval.a) Interval))
+(assert (= (AsNonNullRefField Interval.a Cell) Interval.a))
+(assert (not (= (IsStaticField Interval.b) Smt.true)))
+(assert (= (IsDirectlyModifiableField Interval.b) Smt.true))
+(assert (= (AsRepField Interval.b Interval) Interval.b))
+(assert (= (DeclType Interval.b) Interval))
+(assert (= (AsNonNullRefField Interval.b Cell) Interval.b))
+(assert (subtypes Cell Cell))
+(assert (= (BaseClass_ Cell) System.Object))
+(assert (subtypes Cell (BaseClass_ Cell)))
+(assert (= (AsDirectSubClass Cell (BaseClass_ Cell)) Cell))
+(assert (not (= (IsImmutable_ Cell) Smt.true)))
+(assert (= (AsMutable_ Cell) Cell))
+(assert (subtypes System.Type System.Type))
+(assert (subtypes System.Reflection.MemberInfo System.Reflection.MemberInfo))
+(assert (= (BaseClass_ System.Reflection.MemberInfo) System.Object))
+(assert (subtypes System.Reflection.MemberInfo (BaseClass_ System.Reflection.MemberInfo)))
+(assert (= (AsDirectSubClass System.Reflection.MemberInfo (BaseClass_ System.Reflection.MemberInfo)) System.Reflection.MemberInfo))
+(assert (= (IsImmutable_ System.Reflection.MemberInfo) Smt.true))
+(assert (= (AsImmutable_ System.Reflection.MemberInfo) System.Reflection.MemberInfo))
+(assert (subtypes System.Reflection.ICustomAttributeProvider System.Object))
+(assert (= (IsMemberlessType_ System.Reflection.ICustomAttributeProvider) Smt.true))
+(assert (subtypes System.Reflection.MemberInfo System.Reflection.ICustomAttributeProvider))
+(assert (subtypes System.Runtime.InteropServices._MemberInfo System.Object))
+(assert (= (IsMemberlessType_ System.Runtime.InteropServices._MemberInfo) Smt.true))
+(assert (subtypes System.Reflection.MemberInfo System.Runtime.InteropServices._MemberInfo))
+(assert (= (IsMemberlessType_ System.Reflection.MemberInfo) Smt.true))
+(assert (= (BaseClass_ System.Type) System.Reflection.MemberInfo))
+(assert (subtypes System.Type (BaseClass_ System.Type)))
+(assert (= (AsDirectSubClass System.Type (BaseClass_ System.Type)) System.Type))
+(assert (= (IsImmutable_ System.Type) Smt.true))
+(assert (= (AsImmutable_ System.Type) System.Type))
+(assert (subtypes System.Runtime.InteropServices._Type System.Object))
+(assert (= (IsMemberlessType_ System.Runtime.InteropServices._Type) Smt.true))
+(assert (subtypes System.Type System.Runtime.InteropServices._Type))
+(assert (subtypes System.Reflection.IReflect System.Object))
+(assert (= (IsMemberlessType_ System.Reflection.IReflect) Smt.true))
+(assert (subtypes System.Type System.Reflection.IReflect))
+(assert (= (IsMemberlessType_ System.Type) Smt.true))
+(assert (subtypes PartOfLine PartOfLine))
+(assert (= (BaseClass_ PartOfLine) System.Object))
+(assert (subtypes PartOfLine (BaseClass_ PartOfLine)))
+(assert (= (AsDirectSubClass PartOfLine (BaseClass_ PartOfLine)) PartOfLine))
+(assert (distinct Smt.false Smt.true))
+(assert (let ((?v_0 (select2 Heap_ this ownerFrame_)) (?v_1 (select2 Heap_ this ownerRef_)) (?v_2 (not (= this nullObject))) (?v_3 (not (= stack0o_0 nullObject))) (?v_4 (not (= stack1o_0 nullObject))) (?v_5 (forall ((?o_ Int)) (=> (and (not (= ?o_ nullObject)) (= (= (select2 Heap_ ?o_ allocated_) Smt.true) true)) (and (= (select2 Heap_ ?o_ ownerRef_) (select2 Heap_2_ ?o_ ownerRef_)) (= (select2 Heap_ ?o_ ownerFrame_) (select2 Heap_2_ ?o_ ownerFrame_)))))) (?v_12 (=> true true)) (?v_6 (= ReallyLastGeneratedExit_correct Smt.true)) (?v_7 (= block3553_2_GeneratedUnifiedExit_correct Smt.true)) (?v_15 (= block3553_correct Smt.true)) (?v_14 (= throwException_in Smt.true)) (?v_8 (not (= stack50000o_0 nullObject))) (?v_11 (typeof_ stack50000o_0)) (?v_9 (select2 Heap_1_ stack50000o_0 ownerFrame_)) (?v_10 (select2 Heap_1_ stack50000o_0 ownerRef_)) (?v_13 (= block3468_correct Smt.true)) (?v_19 (= false3451to3468_correct Smt.true))) (let ((?v_21 (=> true ?v_15)) (?v_16 (= block3502_2_block3553_correct Smt.true)) (?v_17 (= block3502_correct Smt.true)) (?v_18 (= true3451to3502_correct Smt.true)) (?v_20 (= block3451_correct Smt.true)) (?v_25 (= false3434to3451_correct Smt.true)) (?v_22 (= block3536_2_block3553_correct Smt.true)) (?v_23 (= block3536_correct Smt.true)) (?v_24 (= true3434to3536_correct Smt.true)) (?v_26 (= block3434_correct Smt.true)) (?v_27 (= block3417_correct Smt.true)) (?v_28 (= entry_correct Smt.true))) (not (=> (=> (=> true (=> (= (IsHeap Heap_) Smt.true) (=> true (=> (= BeingConstructed_ nullObject) (=> (and (or (= ?v_0 PeerGroupPlaceholder_) (not (subtypes (select2 Heap_ ?v_1 inv_) ?v_0)) (= (select2 Heap_ ?v_1 localinv_) (BaseClass_ ?v_0))) (forall ((?pc_ Int)) (let ((?v_29 (typeof_ ?pc_))) (=> (and (not (= ?pc_ nullObject)) (= (= (select2 Heap_ ?pc_ allocated_) Smt.true) true) (= (select2 Heap_ ?pc_ ownerRef_) ?v_1) (= (select2 Heap_ ?pc_ ownerFrame_) ?v_0)) (and (= (select2 Heap_ ?pc_ inv_) ?v_29) (= (select2 Heap_ ?pc_ localinv_) ?v_29)))))) (=> true (=> true (=> (= (IsNotNull_ this Interval) Smt.true) (=> (= (= (select2 Heap_ this allocated_) Smt.true) true) (=> true (=> (=> (=> true (=> true (=> true (=> (=> (=> true (=> true (and ?v_2 (=> ?v_2 (=> (= stack0o_0 (select2 Heap_ this Interval.a)) (and ?v_3 (=> ?v_3 (=> (= stack0i_0 (select2 Heap_ stack0o_0 Cell.Value)) (and ?v_2 (=> ?v_2 (=> (= stack1o_0 (select2 Heap_ this Interval.b)) (and ?v_4 (=> ?v_4 (=> (= stack1i_0 (select2 Heap_ stack1o_0 Cell.Value)) (=> true (=> (and (=> (=> true (=> true (=> true (=> (=> (=> true (=> (= SS_Display.Return.Local_0 local0_0) (=> (= result_0_ local0_0) (=> (= stack50000o_1 stack50000o) (=> (= stack0b_1 local0_0) (=> (= stack0o_1 stack0o_0) (=> (= local0_1 local0_0) (=> (= Heap_2_ Heap_) (=> (=> (=> true (and ?v_5 (=> ?v_5 ?v_12))) ?v_6) ?v_6))))))))) ?v_7) ?v_7)))) ?v_15) (=> (=> true (=> true (=> (> stack0i_0 stack1i_0) (=> true (=> (=> (=> true (=> true (=> true (=> (and (=> (=> true (=> true (=> ?v_14 (=> true (=> (=> (=> true (=> true (=> false (=> (and (= (= (select2 Heap_ stack50000o_0 allocated_) Smt.true) false) ?v_8 (= ?v_11 Microsoft.Contracts.ObjectInvariantException)) (=> (and (= (select2 Heap_ stack50000o_0 ownerRef_) stack50000o_0) (= (select2 Heap_ stack50000o_0 ownerFrame_) PeerGroupPlaceholder_)) (=> (= Heap_0_ (store2 Heap_ stack50000o_0 allocated_ Smt.true)) (and ?v_8 (=> ?v_8 (=> (= (IsHeap Heap_1_) Smt.true) (=> (and (or (= ?v_9 PeerGroupPlaceholder_) (not (subtypes (select2 Heap_1_ ?v_10 inv_) ?v_9)) (= (select2 Heap_1_ ?v_10 localinv_) (BaseClass_ ?v_9))) (= (select2 Heap_1_ stack50000o_0 inv_) Microsoft.Contracts.ObjectInvariantException) (= (select2 Heap_1_ stack50000o_0 localinv_) ?v_11)) (=> (and (= ?v_10 (select2 Heap_0_ stack50000o_0 ownerRef_)) (= ?v_9 (select2 Heap_0_ stack50000o_0 ownerFrame_))) (=> (= (select2 Heap_1_ stack50000o_0 sharingMode_) SharingMode_Unshared_) (=> (forall ((?o_ Int)) (let ((?v_30 (typeof_ ?o_))) (=> (and (not (= ?o_ nullObject)) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) (not true)) (= (= (select2 Heap_1_ ?o_ allocated_) Smt.true) true)) (and (= (select2 Heap_1_ ?o_ inv_) ?v_30) (= (select2 Heap_1_ ?o_ localinv_) ?v_30))))) (=> (forall ((?o_ Int)) (! (let ((?v_31 (select2 Heap_0_ ?o_ FirstConsistentOwner_))) (=> (= (select2 Heap_0_ ?v_31 exposeVersion_) (select2 Heap_1_ ?v_31 exposeVersion_)) (= ?v_31 (select2 Heap_1_ ?o_ FirstConsistentOwner_)))) :pattern ((select2 Heap_1_ ?o_ FirstConsistentOwner_)) )) (=> (forall ((?o_ Int)) (=> (and (not (= ?o_ nullObject)) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) true)) (and (= (select2 Heap_0_ ?o_ ownerRef_) (select2 Heap_1_ ?o_ ownerRef_)) (= (select2 Heap_0_ ?o_ ownerFrame_) (select2 Heap_1_ ?o_ ownerFrame_))))) (=> (forall ((?o_ Int) (?f_ Int)) (! (let ((?v_32 (select2 Heap_0_ ?o_ ownerFrame_)) (?v_33 (select2 Heap_0_ ?o_ ownerRef_))) (=> (and (not (= ?f_ inv_)) (not (= ?f_ localinv_)) (not (= ?f_ FirstConsistentOwner_)) (or (not (= (IsStaticField ?f_) Smt.true)) (not (= (IsDirectlyModifiableField ?f_) Smt.true))) (not (= ?o_ nullObject)) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) true) (or (= ?v_32 PeerGroupPlaceholder_) (not (subtypes (select2 Heap_0_ ?v_33 inv_) ?v_32)) (= (select2 Heap_0_ ?v_33 localinv_) (BaseClass_ ?v_32))) (or (not (= ?o_ stack50000o_0)) (not (subtypes Microsoft.Contracts.ObjectInvariantException (DeclType ?f_)))) true) (= (select2 Heap_0_ ?o_ ?f_) (select2 Heap_1_ ?o_ ?f_)))) :pattern ((select2 Heap_1_ ?o_ ?f_)) )) (=> (forall ((?o_ Int)) (or (= ?o_ stack50000o_0) (and (= (select2 Heap_0_ ?o_ inv_) (select2 Heap_1_ ?o_ inv_)) (= (select2 Heap_0_ ?o_ localinv_) (select2 Heap_1_ ?o_ localinv_))) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) (not true)))) (=> (and (forall ((?o_ Int)) (=> (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) true) (= (= (select2 Heap_1_ ?o_ allocated_) Smt.true) true))) (forall ((?ot_ Int)) (let ((?v_34 (select2 Heap_0_ ?ot_ ownerFrame_))) (=> (and (= (= (select2 Heap_0_ ?ot_ allocated_) Smt.true) true) (not (= ?v_34 PeerGroupPlaceholder_))) (and (= (select2 Heap_1_ ?ot_ ownerRef_) (select2 Heap_0_ ?ot_ ownerRef_)) (= (select2 Heap_1_ ?ot_ ownerFrame_) ?v_34))))) (= (= (select2 Heap_0_ BeingConstructed_ NonNullFieldsAreInitialized_) Smt.true) (= (select2 Heap_1_ BeingConstructed_ NonNullFieldsAreInitialized_) Smt.true))) (=> (forall ((?o_ Int)) (or (= ?o_ stack50000o_0) (= (select2 Heap_0_ ?o_ sharingMode_) (select2 Heap_1_ ?o_ sharingMode_)))) (and ?v_8 (=> ?v_8 (=> false (=> true ?v_12))))))))))))))))))))))) ?v_13) ?v_13))))) ?v_19) (=> (=> true (=> true (=> (not ?v_14) (=> true (=> (=> (=> true (=> true (=> true (=> (=> (=> true (=> (= stack0b_0 throwException_in) (=> (= local0_0 Smt.false) ?v_21))) ?v_16) ?v_16)))) ?v_17) ?v_17))))) ?v_18)) (and ?v_18 ?v_19))))) ?v_20) ?v_20))))) ?v_25) (=> (=> true (=> true (=> (<= stack0i_0 stack1i_0) (=> true (=> (=> (=> true (=> true (=> true (=> (=> (=> true (=> (= stack0b_0 stack0b) (=> (= local0_0 Smt.true) ?v_21))) ?v_22) ?v_22)))) ?v_23) ?v_23))))) ?v_24)) (and ?v_24 ?v_25))))))))))))))))) ?v_26) ?v_26)))) ?v_27) ?v_27))))))))))) ?v_28) ?v_28)))))
+(check-sat)
+(exit)
--- /dev/null
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes () ((Formula!953 (And!954 (lhs!955 Formula!953) (rhs!956 Formula!953)) (Not!957 (f!958 Formula!953)) (Or!959 (lhs!960 Formula!953) (rhs!961 Formula!953)) (Variable!962 (id!963 (_ BitVec 32))))
+))
+(declare-fun error_value!964 () Bool)
+(declare-fun isNNF!208 (Formula!953) Bool)
+(declare-fun error_value!965 () Formula!953)
+(declare-fun nnf!206 (Formula!953) Formula!953)
+(declare-fun error_value!966 () Formula!953)
+(assert (forall ((f!207 Formula!953)) (= (isNNF!208 f!207) (ite (is-And!954 f!207) (and (and (isNNF!208 (lhs!955 f!207)) (isNNF!208 (lhs!955 f!207))) (isNNF!208 (rhs!956 f!207))) (ite (is-Or!959 f!207) (and (and (isNNF!208 (lhs!960 f!207)) (isNNF!208 (lhs!960 f!207))) (isNNF!208 (rhs!961 f!207))) (ite (is-Not!957 f!207) false (ite (is-Variable!962 f!207) true error_value!964))))) ))
+(assert (forall ((formula!205 Formula!953)) (= (nnf!206 formula!205) (ite (is-And!954 formula!205) (And!954 (nnf!206 (lhs!955 formula!205)) (nnf!206 (rhs!956 formula!205))) (ite (is-Or!959 formula!205) (Or!959 (nnf!206 (lhs!960 formula!205)) (nnf!206 (rhs!961 formula!205))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-And!954 (f!958 formula!205))) (Or!959 (nnf!206 (Not!957 (lhs!955 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!956 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Or!959 (f!958 formula!205))) (And!954 (nnf!206 (Not!957 (lhs!960 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!961 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Not!957 (f!958 formula!205))) (nnf!206 (f!958 (f!958 formula!205))) (ite (is-Not!957 formula!205) formula!205 (ite (is-Variable!962 formula!205) formula!205 error_value!965)))))))) ))
+(assert (exists ((formula!205 Formula!953)) (not (=> (is-Variable!962 formula!205) (isNNF!208 (ite (is-And!954 formula!205) (And!954 (nnf!206 (lhs!955 formula!205)) (nnf!206 (rhs!956 formula!205))) (ite (is-Or!959 formula!205) (Or!959 (nnf!206 (lhs!960 formula!205)) (nnf!206 (rhs!961 formula!205))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-And!954 (f!958 formula!205))) (Or!959 (nnf!206 (Not!957 (lhs!955 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!956 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Or!959 (f!958 formula!205))) (And!954 (nnf!206 (Not!957 (lhs!960 (f!958 formula!205)))) (nnf!206 (Not!957 (rhs!961 (f!958 formula!205))))) (ite (and (and (is-Not!957 formula!205) (is-Not!957 formula!205)) (is-Not!957 (f!958 formula!205))) (nnf!206 (f!958 (f!958 formula!205))) (ite (is-Not!957 formula!205) formula!205 (ite (is-Variable!962 formula!205) formula!205 error_value!966)))))))))) ))
+(check-sat)
projects / cvc5.git / commitdiff