Small input doesn't terminate

[keyboardDrummer]

Hey, thanks for reading.

Z3 doesn't terminate, at least not within minutes, on the following input:

(declare-fun |byte#0| () Int)
(set-option :timeout 0)
(assert (not
 (let ((anon0_correct (= (concat #x000000000000000000000000000000 ((_ int2bv 8) |byte#0|)) ((_ int2bv 128) |byte#0|))))
 (=> (and (<= 0 |byte#0|) (<= |byte#0| 255)) anon0_correct))
))
(check-sat)

Is this a bug or am I using it incorrectly?

[aytey]

What happens if you don't have the rlimit line? Also, just to check: do you mean Z3 itself times-out, or that you mean the instance doesn't finish in some time-limit you're controlling from the outside?

Just to make sure you know: 0 for rlimit means "unlimited" (or, at least, it should do, but maybe your issue is saying it doesn't).

[keyboardDrummer]

Thanks :)

What happens if you don't have the rlimit line?

I've removed the rlimit, it doesn't seem to affect the result.

Also, just to check: do you mean Z3 itself times-out, or that you mean the instance doesn't finish in some time-limit you're controlling from the outside?

The latter, I was running it on: https://rise4fun.com/Z3/slU9o

Running it in Z3 directly with (set-option :timeout 0) causes Z3 to hang indefinitely and not return any output. If I configure (set-option :timeout 1000) then it returns unknown.

Is that expected behavior? The input I'm giving it seems pretty simple to solve.

Removing the not causes it to return sat as expected:

(declare-fun |byte#0| () Int)
(set-option :timeout 0)
(assert 
 (let ((anon0_correct (= (concat #x000000000000000000000000000000 ((_ int2bv 8) |byte#0|)) ((_ int2bv 128) |byte#0|))))
 (=> (and (<= 0 |byte#0|) (<= |byte#0| 255)) anon0_correct))
)
(check-sat)

[aytey]

Okay, so the "easy" answer is that some problems are hard for an SMT solver and some are easy -- the size of the instance doesn't mean if something will be hard or easy (I have 3 line files that can take weeks to solve, even though they only use 32-bit numbers).

Your example creates two 128-bit values via int2bv (which isn't actually in SMTLIB, it a Z3 extension); maybe this is just some case that Z3 isn't optimised to solve easily.

Given your original instance (the one with the not) is UNSAT (based on your updated second comment), then it is possible that Z3 has to explore a search-space of ~2^128, which might just be extremely costly to show UNSAT.

[keyboardDrummer]

Alright, thank you very much. As you correctly assessed I don't have a lot of context in this space but this was very educational :)

[keyboardDrummer]

Given the condition (and (<= 0 |byte#0|) (<= |byte#0| 255)), I would hope Z3 only iterates over 256 values. Is this something I could file a bug/feature-request for? I don't think I'm ready to solve this myself any time soon but maybe in time :)

[aytey]

So that's the more difficult part; I would guess that things are "going wrong" because of the int2bv call, which impedes Z3's ability to apply simplifications/reductions/search tactics.

One way to test this would be to declare |byte#0| as either a 128-bit BV or an 8 bit one, adjust your problem with either concat or extract, and then see how quick Z3 solves it ... but, if you do this, you're then solving a very different instance (it would be QF_BV vs. something like QF_BVLIA which your current instance probably is).

[NikolajBjorner]

int2bv and bv2int are not part of SMTLIB standards. It is generally fairly expensive to use.
I have added a helper axiom that could be useful generally and helps with this example. I might have to revert it if it introduces regressions.

[NikolajBjorner]

it does now