Assertion violation at src/util/old_vector.h:375

[wintered]

Triggers the same assertion violation as the fixed issue #3739.

[556] % z3 bug3739.smt2 
(smt.diff_logic: non-diff logic expression (>= (+ b (a c!0)) 0))
unknown
[557] % 
[557] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/util/old_vector.h
Line: 375
idx < size()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[558] % 
[558] % cat small.smt2
(set-option :smt.arith.solver 6)
(set-option :rewriter.push_to_real false)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (forall ((d Int)) (= (/ 1 (- 3 d (ite (= d a) b c))) 0)))
(check-sat)
[559] %

OS: Ubuntu 18.04
Commit: 64d157d

[NikolajBjorner]

Triggers the same assertion violation as the fixed issue #3739.

Sure, but the stacks are widely different.
It is relevant in bug triaging to consider the stack and not just the line of code that asserted/crashed.

[NikolajBjorner]

@levnach - could you take a look at the fix. It amounts to a patch as the object invariants on lar_terms is not what the type signature advertises. The type signature uses tv when iterating over coefficients. The indices are just column indices.
Consider for example lar_solver::add_equality. It converts integers (they should be typed as tv's at this point) to column indices and stores them in terms.
lar_soler::add_term assumes the indices are registered as variables. This is not the case for terms.

[levnach]

When lar_solver consumes a lar_term in "add_term()" it expects all indices be column indices, and it creates also a column that is not reported externally. When returning a lar_term, for example in gomory cutting or bound propogation, it substitutes those columns by the corresponding term indices, masked by tv. Should we have two term types? One external and one internal for lp?

[NikolajBjorner]

Would be better for maintainability and clarity not to have two term types.
The term returned by "get_term" has column indices. The terms returned by the bounds in cuts and branches are (most likely all ) normalized to terms. But normalization is another step which the type system does not capture and lar_term does not know about. In principle a lar_term then has two states, one where the indices are of kind tv, and another where they are some hybrid of column type. This is too error prone.