Fatal failure in cvc5::internal::theory::arith::linear::Comparison::Comparison() at src/theory/arith/linear/normal_form.cpp:657

[cvc5-bot]

cvc5/cvc5@976eba94611f7e2ac3e8ff0791265c2ea1eac4af murxla/murxla@879e44dd9aa77890c5273e970f8b2136b8fb2015

#include <cvc5/cvc5.h>

using namespace cvc5;
int main(void)
{
Solver solver;
solver.setOption("incremental", "false");
solver.setLogic("QF_NRA");
solver.setOption("produce-models", "true");
solver.setOption("incremental", "true");
Sort s0 = solver.getRealSort();
Sort s1 = solver.getBooleanSort();
Sort s2 = solver.getRealSort();
Term t3 = solver.mkConst(s1, "_x0");
Term t4 = solver.mkConst(s0, "_x1");
Term t5 = solver.mkReal(5, 2562);
Term t6 = solver.mkTerm(GEQ, {t4, t5});
Op o7 = solver.mkOp(IMPLIES);
Term t8 = t6.impTerm(t6);
Term t9 = solver.mkVar(s0, "_f2_0");
Term t10 = solver.mkVar(s1, "_f2_1");
Term t11 = solver.mkVar(s0, "_f2_2");
Term t12 = solver.mkVar(s1, "_f2_3");
Op o13 = solver.mkOp(GEQ);
Term t14 = solver.mkTerm(o13, {t9, t11});
Op o15 = solver.mkOp(GT);
Term t16 = solver.mkTerm(o15, {t5, t11});
Term t17 = solver.mkTerm(MULT, {t4, t5});
Term t18 = solver.mkTerm(GEQ, {t17, t5});
Op o19 = solver.mkOp(MULT);
Term t20 = solver.mkTerm(o19, {t17, t17, t17});
Op o21 = solver.mkOp(AND);
Term t22 = t3.andTerm(t6);
Term t23 = solver.mkTerm(GEQ, {t20, t17, t20});
solver.assertFormula(t6);
Sort s24 = solver.getBooleanSort();
Term t25 = solver.mkConst(s0, "_x3");
Term t26 = solver.mkConst(s0, "_x4");
Op o27 = solver.mkOp(LEQ);
Term t28 = solver.mkTerm(o27, {t17, t26});
Term t29 = solver.mkTerm(SUB, {t17, t17});
Term t30 = solver.mkTerm(DIVISION, {t17, t17});
Term t31 = solver.mkTerm(LEQ, {t17, t17});
solver.checkSatAssuming({t3, t3, t23, t28, t3});
solver.blockModel(cvc5::modes::BlockModelsMode::VALUES);
solver.checkSat();

return 0;
}

error:

Fatal failure within cvc5::internal::theory::arith::linear::Comparison::Comparison(cvc5::internal::TNode) at ../src/theory/arith/linear/normal_form.cpp:657
Check failure

 isNormalForm()

[ajreynol]

Likely due to using RAN in model blockers.