search

cvc5 / cvc5-projects

1 stars 0 forks source link

Fatal failure in cvc5::internal::theory::arith::nl::detect_ran_encoding() at src/theory/arith/nl/poly_conversion.cpp:652 #697

Open cvc5-bot opened 7 months ago

cvc5-bot commented 7 months ago

cvc5/cvc5@54f2b125a103114fc39c9d2595603716bee5e41c murxla/murxla@3c45751cb73ce5ff0157aff6783aec3c9000f0f7

(set-option :nl-cov-linear-model persistent)
(set-option :nl-cov true)
(set-option :nl-cov-force true)
(declare-const x Int)
(assert (< 0 x))
(assert (forall ((x4 (_ BitVec 1))) (or (= 0 (int.pow2 x)) (< 80924917 x))))
(check-sat)

error:

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

 w.getKind() == Kind::WITNESS
ajreynol commented 5 months ago

Caused by assigning a model value to (^ 2 <large number>). This does not evaluate but the solver expects a either a concrete value or a witness term.