Fatal failure in cvc5::internal::theory::booleans::TheoryBoolRewriter::computeNnfNorm() at src/theory/booleans/theory_bool_rewriter.cpp:129

[cvc5-bot]

cvc5/cvc5@448b433
murxla/murxla@51f5b5c

(set-option :proof-rewrite-rcons-rec-limit 14966763729191485587)
(set-option :check-proof-steps true)
(declare-const x Real)
(check-sat-assuming ((and (= x (/ 0.0 x)) (= 1.0 (/ 0.0 0.0)))))

error:

Fatal failure within static cvc5::internal::Node cvc5::internal::theory::booleans::TheoryBoolRewriter::computeNnfNorm(cvc5::internal::NodeManager*, const Node&, cvc5::internal::TConvProofGenerator*) at ../src/theory/booleans/theory_bool_rewriter.cpp:129
Check failure

 cur[0].getKind() != Kind::NOT