Optimization combined with a timeout.

[mjp41]

I have been experimenting with the Optimisation feature through a .NET interface. I have added a timeout and it seems to cause issues. The most serious I have experienced is:

ASSERTION VIOLATION
File: ..\..\src\math\lp\int_solver.cpp
Line: 525
Failed to verify: get_freedom_interval_for_column(j, inf_l, l, inf_u, u, m)

Z3 4.8.9.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new

But I have also had

Unhandled exception. Microsoft.Z3.Z3Exception: maximization suspended
   at Microsoft.Z3.Native.Z3_optimize_check(IntPtr a0, IntPtr a1, UInt32 a2, IntPtr[] a3)
   at Microsoft.Z3.Optimize.Check(Expr[] assumptions)
   at LayoutEngine.Program.process_program(IEnumerable`1 prog, UInt32 timeout_ms) in C:\src\LayoutEngine\Program.cs:line 76
   at LayoutEngine.Program.Main(String[] args) in C:\src\LayoutEngine\Program.cs:line 150

C:\src\LayoutEngine\bin\Debug\netcoreapp3.1\LayoutEngine.exe (process 26208) exited with code 0.

and

Unhandled exception. Microsoft.Z3.Z3Exception: push canceled
   at Microsoft.Z3.Native.Z3_optimize_check(IntPtr a0, IntPtr a1, UInt32 a2, IntPtr[] a3)
   at Microsoft.Z3.Optimize.Check(Expr[] assumptions)
   at LayoutEngine.Program.process_program(IEnumerable`1 prog, UInt32 timeout_ms) in C:\src\LayoutEngine\Program.cs:line 76
   at LayoutEngine.Program.Main(String[] args) in C:\src\LayoutEngine\Program.cs:line 149

Failure is non-deterministic between these errors and success.

I have uploaded the complete program that causes the issues:
https://github.com/mjp41/verona_bigtable_test/tree/master

I have not attempted to minimise the program to localise the error, I can do this, if that would be helpful.

[NikolajBjorner]

I tested the update on your snippet. It does not crash any longer.

[mjp41]

Thanks