Unexpected exception "A non-linear fact was asserted to arithmetic in a linear logic." with simplify().

[aniemetz]

cvc5/cvc5@0f5ee6b murxla/murxla@e5e77ae

TEST_F(TestApiBlackSolver, foo)
{
  Solver slv;
  slv.setOption("incremental", "false");
  slv.setOption("solve-int-as-bv", "10516708485319108261");
  Sort s1 = slv.getStringSort();
  Term t1 = slv.mkConst(s1, "_x0");
  Term t12 = slv.mkTerm(Kind::EQUAL, {t1, t1});
  Term t13 = slv.mkTerm(Kind::SET_SINGLETON, {t12});
  Term t28 = slv.mkTerm(Kind::SET_CARD, {t13});
  Term t122 = slv.mkTerm(Kind::MINUS, {t28, t28});
  Term t135 = slv.mkVar(t28.getSort(), "_f12_0");
  Term t136 = slv.mkVar(s1, "_f12_1");
  Term t137 = slv.mkVar(t28.getSort(), "_f12_2");
  Term t138 = slv.mkVar(s1, "_f12_3");
  Term t141 = slv.mkTerm(Kind::INTS_MODULUS, {t122, t122});
  Term t142 = slv.mkTerm(Kind::UMINUS, {t141});
  Term t143 = slv.defineFun("_f12", {t135, t136, t137, t138}, t142.getSort(), t142);
  (void) slv.simplify(t143);
}

Fails with

terminate called after throwing an instance of 'cvc5::api::CVC5ApiException'
  what():  A non-linear fact was asserted to arithmetic in a linear logic.
The fact in question: (let ((_let_1 (set.card (set.singleton (= _x0 _x0))))) (let ((_let_2 (- _let_1 _let_1))) (mod _let_2 _let_2)))

Aborted (core dumped)

[ajreynol]

The issue here I guess is that the user is not setting the logic to linear arithmetic?

The constraints are non-linear, since the INTS_MODULUS has a non-const denominator.

[ajreynol]

Its also strange that simplify would trigger something to be asserted to arithmetic.

[ajreynol]

The message is slightly misleading, perhaps the error message should say A non-linear fact was processed by arithmetic in a linear logic. ?