diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-27 17:27:57 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-27 17:27:57 +0200 |
| commit | 0ddf1b9c74f2b2a78e0960b710c2edbdc5f8d02d (patch) | |
| tree | 523a7c7ec9bfefd4297c5d8f56ef0ff474045d73 /src/theory/strings | |
| parent | d4a7b0cf0500e971c9c01e7628f3c1b567715059 (diff) | |
Do ITE term bookkeeping when solving Sygus inputs. Add missing script from Sygus comp 2015. Fix bug 665 regarding strings rewriter for contains.
Diffstat (limited to 'src/theory/strings')
| -rw-r--r-- | src/theory/strings/theory_strings_rewriter.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp index 7023f7c41..872933cbd 100644 --- a/src/theory/strings/theory_strings_rewriter.cpp +++ b/src/theory/strings/theory_strings_rewriter.cpp @@ -948,8 +948,9 @@ RewriteResponse TheoryStringsRewriter::postRewrite(TNode node) { bool flag = false; unsigned n1 = node[0].getNumChildren(); unsigned n2 = node[1].getNumChildren(); - if(n1 - n2) { - for(unsigned i=0; i<=n1 - n2; i++) { + if( n1>n2 ){ + unsigned diff = n1-n2; + for(unsigned i=0; i<diff; i++) { if(node[0][i] == node[1][0]) { flag = true; for(unsigned j=1; j<n2; j++) { |