Max-SMT from C# API

[calebh]

I recently switched over to using the C# API from Python and am having trouble with forcing Z3 to use a Max-SMT algorithm. The full model that I am optimizing over is available here: https://gist.github.com/calebh/bef99d9fee55f0be0bd93debea840d58

As you can see all of the hard inequalities are simple constraints against constant and are therefore linear. Since this is a minimization problem I am attempting to minimize over the negation of the variables.

Running the model from above in the Z3 command line works perfectly fine. On the C# side I get the following error:
Exception thrown at 0x00007FFF0B364F69 in DataLabeling.exe: Microsoft C++ exception: opt::context::is_fd::found_fd at memory location 0x0000001853DADA70.

Code is here: https://github.com/calebh/data-labeling/blob/master/DataLabeling/Synthesize.cs#L141

The context is created earlier in that function.

Is there some sort of flag I have to tell Z3 to use in order to get it to use the right solver? Does fd mean the solver that Z3 is using? Am I going about this in the proper way?

I also need some way to get what the soft objectives add up to.

[NikolajBjorner]

The exception is internal. It shouldn't be raised outside of the z3 library. It is caught internally.
If the exception leaks there has to be some binary incompatibility.

My debug console in the VS debugger contains the following information:

'DataLabeling.exe' (Win32): Loaded 'C:\Windows\System32\vcruntime140.dll'.
'DataLabeling.exe' (Win32): Loaded 'C:\Windows\System32\vcruntime140_1.dll'.
Exception thrown at 0x00007FFD8F434F69 in DataLabeling.exe: Microsoft C++ exception: opt::context::is_fd::found_fd at memory location 0x0000009D4E57D810.
Exception thrown at 0x00007FFD8F434F69 in DataLabeling.exe: Microsoft C++ exception: opt::context::is_fd::found_fd at memory location 0x0000009D4E57D810.
The thread 0x8dc4 has exited with code 0 (0x0).
The thread 0xbb8c has exited with code 0 (0x0).
The thread 0xee00 has exited with code 0 (0x0).

The output on the newest version of your code is two calls resulting in usat and two calls resulting in sat.
You can reproduce with text by dumping state of the solver s:

  Action<Optimize, Ir> runZ3 = (Optimize s, Ir nf) => {
                            Console.WriteLine($"{s}");

[calebh]

It looks like all the native code debug options I had turned on in Visual Studio were catching the internal exceptions. I enabled "Just my code" and turned off native code debugging in the project settings and it is working now.