Skip to content

Fix instance of no rewrite in extended rewriter#6610

Merged
4tXJ7f merged 1 commit intocvc5:masterfrom
ajreynol:fix6645
May 24, 2021
Merged

Fix instance of no rewrite in extended rewriter#6610
4tXJ7f merged 1 commit intocvc5:masterfrom
ajreynol:fix6645

Conversation

@ajreynol
Copy link
Copy Markdown
Member

Fixes #6545.

An assertion failure was being raised indicating that we were reporting a rewrite that was not changing the original term.

@ajreynol ajreynol added minor Priority simple Complexity labels May 24, 2021
@ajreynol ajreynol requested a review from 4tXJ7f May 24, 2021 15:08
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

@4tXJ7f 4tXJ7f merged commit 93a3d6a into cvc5:master May 24, 2021
@ajreynol ajreynol deleted the fix6645 branch May 24, 2021 16:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

minor Priority simple Complexity

Projects

None yet

Development

Successfully merging this pull request may close these issues.

(ext-rew-prep, ext-rew-prep-agg) Fatal failure at src/theory/quantifiers/extended_rewrite.cpp:229

2 participants