Patrick LaFontaine

I saw this issue again, unfortunately I'm not sure this is the right venue for these kinds of questions: - It depends on the logic you are working with and...

I don't have the full sense what you are attempting to do but I'll point out what I think are a few misconceptions to hopefully guide you down the right...

In doing some more digging, I see that Z3 tries to warn the user about this but in #92 we disabled the error handler and don't otherwise try to detect...

The changes look good to me. Are you asking about diffing the windows linking issue?

FWIW I tried building z3 using github actions with 4.12.4 and still ran into this issue. https://github.com/Pat-Lafon/z3.rs/actions/runs/7215253276/job/19659127883?pr=2

I was trying a couple different commits and I think I narrowed down the issue to this commit: https://github.com/Z3Prover/z3/commit/9d3fef3e2bdf6d1806aa9c2b171b1bb6f9d41d2f . The previous commit in the history seems to pass but...

The original comment might need a little bit more elaboration. The original pr #88 which added these operations specifically called out shr as the BV operation not to be added...

I saw this and thought it was interesting so I gave a crack at it. Instead of creating an iterator over solutions, I created an iterator over models. Two things...

One example of hitting this is if you create a function application that doesn't typecheck. For example: ```rust let f = FuncDecl::new(&ctx, "f", &[&Sort::int(&ctx)], &Sort::int(&ctx)); let y = String::new_const(&ctx, "y");...

I think this is best described as the [Interior Mutability Pattern](https://doc.rust-lang.org/book/ch15-05-interior-mutability.html#refcellt-and-the-interior-mutability-pattern) since all objects are secretly reference counted on the Z3 c side of things.