search

cvc5 / cvc5-projects

1 stars 0 forks source link

Fatal failure in nl::detect_ran_encoding() at src/theory/arith/nl/poly_conversion.cpp:667 #400

Closed mpreiner closed 2 years ago

mpreiner commented 2 years ago

cvc5/cvc5@acba73710 murxla/murxla@4f03339

(set-logic ABVNRAT)
(declare-const x Real)
(declare-const _x Real)
(declare-const x1 Real)
(assert (ite (= 0.0 real.pi) false (= (= x (- _x)) (= 0.0 (/ 0.0 x1 0.0)))))
(check-sat)

error:

Fatal failure within std::tuple<cvc5::NodeTemplate<true>, cvc5::Rational, cvc5::Rational> cvc5::theory::arith::nl::detect_ran_encoding(const Node&) at src/theory/arith/nl/poly_conversion.cpp:667
Check failure

 n.getKind() == Kind::AND
Invalid node structure.
nafur commented 2 years ago

We will soon use proper RealAlgebraicNumber nodes, making the incorrect code obsolete.

nafur commented 2 years ago

This issue was resolved by cvc5/cvc5#7939 and cvc5/cvc5#8076.