search

cvc5 / cvc5-projects

1 stars 0 forks source link

Fatal failure in cvc5::internal::theory::Rewriter::rewriteTo() at src/theory/rewriter.cpp:321 #710

Open cvc5-bot opened 2 months ago

cvc5-bot commented 2 months ago

cvc5/cvc5@0202c0d9ddb44e1b05bc914230683dc2ff16d23a murxla/murxla@51f5b5c05abaeb7a463f7ca8d1e8c6489dec1c02

(declare-const __ (_ BitVec 1))
(set-option :check-proof-steps true)
(assert (ite (bvuge (_ bv0 74) (bvsdiv ((_ zero_extend 73) __) (_ bv9444732965739290427392 74))) false true))
(check-sat)

error:

Fatal failure within cvc5::internal::Node cvc5::internal::theory::Rewriter::rewriteTo(cvc5::internal::theory::TheoryId, cvc5::internal::Node, cvc5::internal::TConvProofGenerator*) at ../src/theory/rewriter.cpp:321
Check failure

 d_rewriteStack->find(response.d_node) == d_rewriteStack->end()
ajreynol commented 2 months ago

Likely fixed by https://github.com/cvc5/cvc5/pull/10641.