Unexpected behavior when trying to minimize bitvector

[danielrainer]

I have code which builds up some constraints over bitvectors and then tries to minimize the value of one of them. Code to reproduce the issue can be found at https://github.com/danielrainer/z3_rust_minimize_repro

What I expected my code to do:

• Set up some constraints over bitvectors (in this case read from a SMT-LIB string)
• Add the requirement to minimize the value of one of the bitvectors
• Find a model where the bitvector which should be minimized has minimal value
• The loop at the end should not be necessary, but when present, it should have the same effect as automatic minimization

What happens:

• The first model found has a non-minimized value of #x0000d72b44f15e6d for the relevant bitvector.
• The model found by decreasing the upper limit on the bitvector until the constraints become unsatisfiable finds the minimized value #x0000d72b44b15e6d (which is different at bit index 22, f vs b)

Am I misusing the API, do I misunderstand some semantics, or is this a bug?

For reference, the version of Z3 installed on my system is

Z3 version 4.13.0 - 64 bit - build hashcode 3049f578a8f98a0b0992eca193afe57a73b30ca3

When I extend the constraints file by appending

(minimize initial_a)
(check-sat)
(get-model)

and directly invoking Z3 from the command line, the resulting model has the expected value of #x0000d72b44b15e6d.