Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Fatal failure within CVC4::theory::RewriteResponse (QF_ABVFP formula) #3536

Closed
wintered opened this issue Dec 6, 2019 · 0 comments · Fixed by #3548
Closed

Fatal failure within CVC4::theory::RewriteResponse (QF_ABVFP formula) #3536

wintered opened this issue Dec 6, 2019 · 0 comments · Fixed by #3548
Assignees
@4tXJ7f

Comments

@wintered
Copy link

wintered commented Dec 6, 2019

Hi,
Consider the following formula:

(declare-fun symbolic_0_double_12660 () (Array (_ BitVec 32) (_ BitVec 8)))
(assert
 (let ((?x12 (concat (select symbolic_0_double_12660 (_ bv1 32)) (select symbolic_0_double_12660 (_ bv0 32)))))
(let ((?x18 (concat (select symbolic_0_double_12660 (_ bv3 32)) (concat (select symbolic_0_double_12660 (_ bv2 32)) ?x12))))
(let ((?x24 (concat (select symbolic_0_double_12660 (_ bv5 32)) (concat (select symbolic_0_double_12660 (_ bv4 32)) ?x18))))
(let ((?x30 (concat (select symbolic_0_double_12660 (_ bv7 32)) (concat (select symbolic_0_double_12660 (_ bv6 32)) ?x24))))
(let (($x38 (= true (fp.geq ((_ to_fp 11 53) ?x30) ((_ to_fp 11 53) (_ bv13831004815617530266 64))) (fp.leq ((_ to_fp 11 53) ?x30) ((_ to_fp 11 53) (_ bv4607632778762754458 64))))))
(not (distinct true $x38))))))))
(check-sat)

CVC4 crashes on it with the following error message:

Fatal failure within CVC4::theory::RewriteResponse CVC4::theory::fp::rewrite::removed(CVC4::TNode, bool) at /home/windomin/project_share/solver_binaries/cache/CVC4/src/theory/fp/theory_fp_rewriter.cpp:157
Unreachable code reachedkind (FLOATINGPOINT_TO_FP_GENERIC) should have been removed?

Revision: 46eeb6a
OS: Ubuntu 18.04
@4tXJ7f 4tXJ7f self-assigned this Dec 8, 2019
4tXJ7f added a commit to 4tXJ7f/cvc5 that referenced this issue Dec 9, 2019
@4tXJ7f
Avoid calling rewriter from type checker
6be3e6d 
Fixes cvc5#3536. The type checker for the chain operator was calling the
rewriter. However, the floating-point rewriter was expecting
`TheoryFp::expandDefinition()` to be applied before rewriting. If the
chain operator had subterms that were supposed to be removed by
`TheoryFp::expandDefinition()`, the FP rewriter was throwing an
exception. This commit fixes the issue by not calling the full rewriter
in the type checker but by just expanding the chain operator. This is a
bit less efficient than before because the rewriter does not cache the
result of expanding the chain operator anymore but assuming that there
are no long chains, the performance impact should be negligible. It also
seemed like a reasonable assumption that the rewriter can expect to run
after `expandDefinition()` because otherwise the rewriter has to expand
definitions, which may be too restrictive.
@4tXJ7f 4tXJ7f mentioned this issue Dec 9, 2019
Merged
4tXJ7f added a commit that referenced this issue Dec 18, 2019
@4tXJ7f
Avoid calling rewriter from type checker (#3548)
9c2c058 
Fixes #3536. The type checker for the chain operator was calling the
rewriter. However, the floating-point rewriter was expecting
`TheoryFp::expandDefinition()` to be applied before rewriting. If the
chain operator had subterms that were supposed to be removed by
`TheoryFp::expandDefinition()`, the FP rewriter was throwing an
exception. This commit fixes the issue by not calling the full rewriter
in the type checker but by just expanding the chain operator. This is a
bit less efficient than before because the rewriter does not cache the
result of expanding the chain operator anymore but assuming that there
are no long chains, the performance impact should be negligible. It also
seemed like a reasonable assumption that the rewriter can expect to run
after `expandDefinition()` because otherwise the rewriter has to expand
definitions, which may be too restrictive.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@4tXJ7f 4tXJ7f

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Avoid calling rewriter from type checker 4tXJ7f/cvc5
2 participants
@4tXJ7f @wintered