diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-01-30 11:20:29 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-01-30 11:20:29 -0600 |
| commit | 0dd2aa21f35b221ea96d277e9ea7cbc816ffe83c (patch) | |
| tree | 3aa2c1df2c732643c3ca95620fcf38e8e5608af8 /src/theory/strings/theory_strings.h | |
| parent | a8a7949ec3e1a7f2a2d241d0fc58e08cbf4b7aec (diff) | |
Fix regexp cache issue in strings, add regression.
Diffstat (limited to 'src/theory/strings/theory_strings.h')
| -rw-r--r-- | src/theory/strings/theory_strings.h | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 457afb15a..0294c3884 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -359,9 +359,7 @@ private: std::map< Node, std::vector< Node > > &XinR_with_exps); void checkMemberships(); bool checkMemberships2(); - bool checkPDerivative( Node x, Node r, Node atom, bool &addedLemma, - std::vector< Node > &processed, std::vector< Node > &cprocessed, - std::vector< Node > &nf_exp); + bool checkPDerivative( Node x, Node r, Node atom, bool &addedLemma, std::vector< Node > &nf_exp); //check contains void checkPosContains( std::vector< Node >& posContains ); void checkNegContains( std::vector< Node >& negContains ); |