Skip to content

Fix indexof_re reduction#8065

Merged
4tXJ7f merged 5 commits intocvc5:masterfrom
ajreynol:fixIndexOfReRed
Feb 7, 2022
Merged

Fix indexof_re reduction#8065
4tXJ7f merged 5 commits intocvc5:masterfrom
ajreynol:fixIndexOfReRed

Conversation

@ajreynol
Copy link
Copy Markdown
Member

@ajreynol ajreynol commented Feb 4, 2022

Fixes #6654.

Note that this regression now answers unknown with --ext-rewrite-quant; the regression without this option is added.

@ajreynol ajreynol added normal Priority simple Complexity labels Feb 4, 2022
@ajreynol ajreynol requested a review from 4tXJ7f February 4, 2022 22:31
Copy link
Copy Markdown
Member

@4tXJ7f 4tXJ7f left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, nice find.

@4tXJ7f 4tXJ7f enabled auto-merge (squash) February 7, 2022 17:04
@4tXJ7f 4tXJ7f merged commit f4b167e into cvc5:master Feb 7, 2022
@ajreynol ajreynol deleted the fixIndexOfReRed branch March 9, 2022 18:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

normal Priority simple Complexity

Projects

None yet

Development

Successfully merging this pull request may close these issues.

(ext-rewrite-quant, full-saturate-quant) refutation unsoundness on string formula

2 participants