Some invalidation logic is missing.

[MAKMED1337]

#include <iostream>
#include <z3++.h>

using namespace z3;
using namespace std;

int main() {
    context c;
    solver s(c);

    auto a = c.real_const("a");
    s.add(a <= 1);

    auto f = c.real_const("f");
    s.add(f >= 2);

    auto t = c.real_const("t");
    s.add(f == t + a);

    s.push();
    s.add(t == 0);
    cerr << s.check() << "\n";
    s.pop();

    auto m = s.get_model();
}

Tested on both 4.15.4.0 and the git versions.
It crashes with:

unsat
ASSERTION VIOLATION
File: /usr/src/debug/z3/z3/src/math/lp/lar_solver.cpp
Line: 1557
Failed to verify: m_imp->m_columns_with_changed_bounds.empty()

4.15.4.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
terminate called after throwing an instance of 'z3::exception'
  what():  unreachable

And the same goes for the git version:

unsat
ASSERTION VIOLATION
File: ../src/math/lp/lar_solver.cpp
Line: 1563
Failed to verify: m_imp->m_columns_with_changed_bounds.empty()

Z3 4.17.0.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
terminate called after throwing an instance of 'z3::exception'
  what():  unreachable

It should drop the model after the pop, but it doesn't.

[levnach]

I think there is no promise that the model is restored on the pop(). Calling s.check() between s.pop() and s.get_model() fixes the crash.

[MAKMED1337]

I am not saying that it should restore, but usually it errors out with there is no current model after the pop. And here it asks me to report the error and exits the program, so I cannot catch it.