Unexpected response to get-info :reason-unknown: "can't tell"

[nafur]

It s seems that yices enters an incorrect state when it answers unknown due to a timeout. As an example take the following input, though I guess it doesn't really matter:

(set-logic QF_UFLIA)
(declare-const x Bool)
(declare-fun >> (Int) Int)
(declare-fun R () Int)
(declare-fun n (Int Int) Int)
(declare-fun u (Int Int) Int)
(assert (= 0 (u (u 1 0) (ite x (mod (n (>> R) 1) 883423532389192329425295078641595165347425375163663761336906547) 0))))
(assert (= (u 1 (ite x 0 (n (>> R) 1))) (mod (ite false 0 (n (>> R) 1)) 34359)))
(check-sat)
(get-info :reason-unknown)

This is what happens on my machine, but we have also seen it on macos:

$ ./yices-smt2 --version
Yices 2.6.5
Copyright SRI International.
Linked with GMP 6.2.1
Copyright Free Software Foundation, Inc.
Build date: 2024-07-31
Platform: x86_64-pc-linux-gnu (release/static)
Revision: 8e6297e233299631147f98659224c3118fc6a215
$ ./yices-smt2 --incremental --timeout 2 out.smt2
... 2 seconds pass ...
unknown
(error "can't tell until you call (check-sat)")

I would expect something like (reason "timeout") maybe, but definitely not an error...