Closed
Description
I'm curious why the following benchmark:
(set-logic QF_ABV)
(define-fun s1 () (Array (_ BitVec 1) (_ BitVec 1)) (store (store ((as const (Array (_ BitVec 1) (_ BitVec 1))) #b0) #b0 #b0) #b1 #b1))
(define-fun s3 () (Array (_ BitVec 1) (_ BitVec 1)) (store (store ((as const (Array (_ BitVec 1) (_ BitVec 1))) #b1) #b0 #b0) #b1 #b1))
(assert (distinct s1 s3))
(check-sat)
(get-info :reason-unknown)
causes z3 to respond unknown, with the reason:
unknown
(:reason-unknown "smt tactic failed to show goal to be sat/unsat (incomplete (theory array))")
If you change the logic to ALL, it correctly responds unsat.
While this isn't necessarily a big deal, I'm curious why QF_ABV logic isn't able to decide this rather simple query.
(Not that it's relevant; but cvc5 returns unsat with either logic.)
Metadata
Assignees
Labels
No labels