proved assertion and its negation

[j123123]

(set-logic ALL)

; Hyperoperation
(define-fun-rec hyper ((a Int) (n Int) (b Int)) Int
  (ite (= n 0) (+ b 1)
    (ite (and (= n 1) (= b 0)) a
      (ite (and (= n 2) (= b 0)) 0
        (ite (and (>= n 3) (= b 0)) 1
          (hyper a (- n 1) (hyper a n (- b 1)) )
        )
      )
    )
  )
)

(push)
(assert
  (= (hyper 0 1 (- 1)) 10 )
)
(check-sat)
(pop)

(push)
(assert
  (not (= (hyper 0 1 (- 1)) 10 ))
)
(check-sat)
(pop)

(push)
(assert
  (=
     (= (hyper 0 1 (- 1)) 10 )
     (not (= (hyper 0 1 (- 1)) 10 ))
  ) 
)
(check-sat)
(pop)

(exit)

Output:

sat
sat
unsat

I think this is bug.

[NikolajBjorner]

hyper isn't terminating; the definition isn't well formed. Z3 does not tell you that you defined a non-terminating function. It makes no such checks and check-sat can produce arbitrary answers in this case.

[j123123]

and check-sat can produce arbitrary answers in this case.

Why? Why not produce "unknown" answer?

[NikolajBjorner]

I find proof assistants are more suitable for checking consistency of recursive definitions because they basically need to accept or find a well-founded ordering. The SMT-LIB analogue would be to annotate with some well-founded ordering and then produce auxiliary proof obligations for these, and in the common case of primitive recursive functions just figure out that they are well-formed. But this functionality is replicated in program verification environments and interactive provers that support problem decomposition.