adding simple new constraint causes optimizer to fail or hang

Question

I've a small-medium sized problem I've modeled using the python bindings to z3.

It is effectively a loan scenario calculator. I've had it working with a test suite for a while now and have recently added a new condition around how interest rate varies (increases) as the loan size increases compared to the value of the collateral ("loan to value or ltv").

In my case the loan-to-value is a potential source for optimization as we can either change the value of the collateral by buying something different or change the value of the loan by putting down a larger down payment. Stating this in order to avoid pasting my entire file here for brevity.

Here's a snippet of what I've always had, working:

loan_payment = Real("loan_payment")
s.add(loan_payment >= 0)

loan_amount = Real("loan_amount")
s.add(loan_amount > 0)
s.add(loan_amount < actual_price) # actual price is passed in as an int

financed_amount = Real("financed_amount")
s.add(financed_amount > 0)
s.add(financed_amount < actual_price)  # sanity

s.add(loan_to_value == loan_amount / financed_amount)

s.add(
    loan_payment
    == (
        (monthly_interest_rate * (1 + monthly_interest_rate) ** 360)
        / ((1 + monthly_interest_rate) ** 360 - 1)
        * loan_amount
    )
)

There are few more constraints for financed_amount and loan_amount which define the boundaries and sources for that money, a bit irrelevant I think however.

What I have newly introduced is:

monthly_interest_rate = Real("monthly_interest_rate")

s.add(
    Implies(
        loan_to_value > 0.8,
        monthly_interest_rate == 6.78 / (12.0 * 100),
    )
)
s.add(
    Implies(
        loan_to_value <= 0.8,
        monthly_interest_rate == 6.78 / (12.0 * 100),
    )
)

This itself is a reduced also failing example of the actual code (I get the rates dynamically).

The former code simply passed in a fixed rate (6.78) into the function, so it was not a z3.Real prior, it was:

monthly_interest_rate = fixed_rate / (12.0 * 100)

The newly introduced code causes my test suite to fail, even though the monthly_interest_rate is identical for either implication (I did that as a sanity check, but it is still failing).

More strangely, to me a novice at z3, is that when I further reduce the new code to:

monthly_interest_rate == (6.78 / (12.0 * 100))

Not only does the code not work, still, the test suite just hangs.

Why is introducing this additional Real breaking my optimizer?