Solver returns SAT and model for which one of the assertions evals to false

Jun 3, 2014 at 5:27 PM
Edited Jun 3, 2014 at 5:30 PM
For a certain problem that I ran through Z3 I get SAT and a model. But when I run
this evaluates to false! Is this ever an expected case? The model indeed appears to not satisfy the assertions I made.

I am using Push and Pop, but not between the call to Check and the call to Eval. I'm using the .NET API in version

The solver was created with MkSimpleSolver. I am not using assumptions. The formula has BVs, integers and propositional terms. No quantifiers. The context has the following creation code:
            var settings = new Dictionary<string, string>()
                { "model", "true" },
                { "MBQI", "true" },
                { "MBQI_MAX_ITERATIONS", "1000000" },
            return new Context(settings);
Jun 4, 2014 at 1:14 PM
Thanks for reporting this issue! If solver.Assertions are the assertions that are being solved then yes, we wouldn't expect the evaluation to fail. However, from the information here I can't tell where the problem lies. Before we dig deeper, could you try switching to the unstable branch (either compile it yourself or use one of the pre-built binaries in the download section under `Planned'). There have been many bugfixes that are not in the main branch or binaries yet, and it's quite possible that we've already fixed the underlying problem.
Jun 5, 2014 at 4:11 PM
It's not fixed on which I just tried. How can I send you a repro? I'll try your mail address which I found.
Jun 5, 2014 at 4:30 PM
I have sent a repro to your Microsoft mail address. Let me know if this is enough to troubleshoot.
Jun 6, 2014 at 1:52 PM
Thanks a lot! I can confirm, the bug also occurs on my machine, but I don't have a solution just yet.
Jun 9, 2014 at 3:04 PM
Thanks again, there was indeed a bug in our bit-blaster which is now fixed (as of this commit). Could you verify that this fixes the problem for you?
Jun 9, 2014 at 5:11 PM
The bug is fixed. Thank you very much! Short time-to-fix.