Assertion failure at solvers/simplex/simplex.c:10349

[mpreiner]

The following yices_push(ctx) call produces the below error with a debug build commit 09f162107cc9140172e6c890d8ccc633126c3720.

#include "yices.h"

int
main()
{
  yices_init();
  type_t s1 = yices_real_type();
  term_t t1 = yices_new_uninterpreted_term(s1);
  term_t t2 = yices_new_uninterpreted_term(s1);
  term_t z = yices_parse_rational("0");
  term_t a1 = yices_arith_gt_atom(t2, z);
  term_t a2 = yices_arith_leq_atom(t2, t1);
  term_t a3 = yices_arith_lt_atom(t1, z);

  ctx_config_t* cfg = yices_new_config();
  context_t* ctx = yices_new_context(cfg);

  yices_assert_formula(ctx, a1);
  yices_assert_formula(ctx, a2);
  yices_assert_formula(ctx, a3);
  yices_check_context_with_assumptions(ctx, NULL, 1, &a2);
  yices_push(ctx);

  return 0;
}

error:

solvers/simplex/simplex.c:10349: simplex_push: Assertion `solver->decision_level == solver->base_level && solver->bstack.prop_ptr == solver->bstack.fix_ptr && solver->save_rows && eassertion_queue_is_empty(&solver->egraph_queue)' failed.