(interpolants) Fatal failure in void cvc5::TheoryEngine::preRegister() at src/theory/theory_engine.cpp:291.

[aniemetz]

cvc5/cvc5@0f5ee6bb4a4477d40d7f6577ea0c5bac17420935 murxla/murxla@f5e3c493b51bfcb5a3e99b06f482556a2534c213

TEST_F(TestApiBlackSolver, barr)
{
  Solver slv;
  slv.setLogic("UFBVFP");
  slv.setOption("produce-interpols", "default");
  slv.setOption("incremental", "false");
  Sort s4 = slv.mkBitVectorSort(39);
  Term t3 = slv.mkVar(s4, "_x2");
  Term t26;
  {
    uint32_t bw = s4.getBitVectorSize();
    t26 = slv.mkBitVector(bw, std::string(bw, '1'), 2);
  }
  Term t38 = slv.mkConst(s4, "_x24");
  Term t60 = slv.mkTerm(Kind::BITVECTOR_UREM, {t3, t26});
  Term t63 = slv.mkTerm(Kind::BITVECTOR_REDOR, {t60});
  Term t64 = slv.mkTerm(Kind::BITVECTOR_UGT, {t26, t38});
  Term t66 = slv.mkTerm(Kind::EQUAL, {t64, t63});
  slv.assertFormula({t64});
  {
    Term ipol;
    bool success = slv.getInterpolant(t66, ipol);
    if (slv.getOption("incremental") == "true")
    {
      while(success)
      {
        success = slv.getInterpolantNext(ipol);
      }
    }
  }
}

Fails with

Fatal failure within void cvc5::TheoryEngine::preRegister(cvc5::TNode) at src/theory/theory_engine.cpp:291
Unhandled case encountered Preregistered term with free variable: (forall ((__internal_interpol (-> (_ BitVec 39) (_ BitVec 39) Bool))) (not (forall ((BOUND_VARIABLE_313 (_ BitVec 39)) (BOUND_VARIABLE_315 (_ BitVec 39))) (let ((_let_1 (bvult BOUND_VARIABLE_313 #b111111111111111111111111111111111111111))) (let ((_let_2 (__internal_interpol BOUND_VARIABLE_313 BOUND_VARIABLE_315))) (and (or (not _let_1) _let_2) (or (not _let_2) (= (not (= #b000000000000000000000000000000000000000 (bvurem _x2 #b111111111111111111111111111111111111111))) _let_1))))))) ), fv=_x2
Aborted (core dumped)

This should not fail with an assertion failure (but should ultimately throw a Cvc5ApiException).

[merlinsun]

This is another instance related to solve-bv-as-int. Since I find solve-bv-as-int is not a regular option now, I'm not sure if it has some values.

$ cvc5 delta.smt2 --solve-bv-as-int=sum
delta.smt2:1.11: No set-logic command was given before this point.
delta.smt2:1.11: cvc5 will make all theories available.
delta.smt2:1.11: Consider setting a stricter logic for (likely) better performance.
delta.smt2:1.11: To suppress this warning in the future use (set-logic ALL).
Fatal failure within void cvc5::internal::TheoryEngine::preRegister(cvc5::internal::TNode) at /root/cvc5/src/theory/theory_engine.cpp:291
Unhandled case encountered Preregistered term with free variable: (>= (__intblast_fun_b_int_2 x_int) 0), fv=x_int
Aborted (core dumped)
$ cat delta.smt2
(declare-fun b ((_ BitVec 1)) (_ BitVec 1))
(assert (forall ((x (_ BitVec 1))) (= (b x) (b (_ bv0 1)))))
(check-sat)