diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-28 14:57:59 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-28 14:57:59 +0200 |
| commit | 187e5d57adeda59c8899321c882db1d5b9a6f2ba (patch) | |
| tree | 65d3e845aecddc5ce9c7f89ac01d4370b9299465 | |
| parent | da790d921114f250597606313245f9fe7fcb72d5 (diff) | |
Minor fix
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 4a1001a04..a66eeffc3 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1207,6 +1207,7 @@ bool TheoryStrings::processLoop(std::vector< Node > &antec, return true; } Node TheoryStrings::mkSkolemSplit( Node a, Node b, const char * c, int isLenSplit ){ + //return mkSkolemS( c, isLenSplit ); std::map< int, Node >::iterator it = d_skolem_cache[a][b].find( isLenSplit ); if( it==d_skolem_cache[a][b].end() ){ Node sk = mkSkolemS( c, isLenSplit ); @@ -1215,6 +1216,7 @@ Node TheoryStrings::mkSkolemSplit( Node a, Node b, const char * c, int isLenSpli }else{ return it->second; } + } bool TheoryStrings::processNEqc(std::vector< std::vector< Node > > &normal_forms, @@ -3328,13 +3330,14 @@ bool TheoryStrings::checkExtendedFuncsEval() { } }else{ if( !areEqual( n, nrc ) ){ - expl = mkExplain( exp ); if( n.getType().isBoolean() ){ exp.push_back( nrc==d_true ? n.negate() : n ); + //exp.push_back( n ); conc = d_false; }else{ conc = n.eqNode( nrc ); } + expl = mkExplain( exp ); } } if( !conc.isNull() ){ |