Z3 incorrect sat response with sequences

[OrenGitHub]

Hi,
This may (or may not) be related to #2447 (crash.smt), as it is almost identical to it:

$ diff crash.smt bug.smt
54c54
< 					(<  j 1))
---
> 					(<  j n))

The following code returns an incorrect sat answer:

;;;;;;;;;;;;;;;;;;;;;;;;;;;
;                         ;
; some arbitrary sequence ;
;                         ;
;;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const A (Seq Int))

;;;;;;;;;;;;;
;           ;
; max index ;
;           ;
;;;;;;;;;;;;;
(declare-const m Int)

;;;;;;;;;;;;;;;;;;;;;;;;;
;                       ;
; max index constraints ;
;                       ;
;;;;;;;;;;;;;;;;;;;;;;;;;
(assert (<= 0 m))
(assert (< m (seq.len A)))
(assert (forall ((i Int)) (<= (seq.nth A i) (seq.nth A m))))

;;;;;;;;;;;;;;;;;;;;;;;;;;
;                        ;
; the projected sequence ;
;                        ;
;;;;;;;;;;;;;;;;;;;;;;;;;;
(declare-const f_A (Seq Int))
(assert (= f_A
	(let (
		(max (seq.nth A m))
		(n   (seq.len A)))
	(ite
		(or (>= max n) (< max 0))
		(seq.unit 74)
		(seq.++
			(seq.extract A 0 m)
			(seq.extract A (+ m 1) (- (- n 1) m)))))))

;;;;;;;;;;;;;;;;;
;               ;
; specification ;
;               ;
;;;;;;;;;;;;;;;;;
(define-fun spec ((in (Seq Int))) Bool
	(let (
		(n (seq.len in)))
	(and
		(forall ((j Int))
			(=>
				(and
					(<= 0 j)
					(<  j n))
				(and
					(<= 0 (seq.nth in j))
					(<  (seq.nth in j) n))))))
)

;;;;;;;;;;;;;;;;;;;;;;;;;;
;                        ;
; specification property ;
;                        ;
;;;;;;;;;;;;;;;;;;;;;;;;;;
(assert (and (spec f_A) (not (spec A))))

;;;;;;;;;
;       ;
; debug ;
;       ;
;;;;;;;;;
(declare-const spec_f_A Bool)
(assert (= (spec f_A) spec_f_A))

;;;;;;;;;;;;;;;;;;;;;;
;                    ;
; initial conditions ;
;                    ;
;;;;;;;;;;;;;;;;;;;;;;
(assert (< 2 (seq.len A)))
(assert (< (seq.len A) 5))

;;;;;;;;;;;;;;;;;;;;;;;;;
;                       ;
; check sat + get model ;
;                       ;
;;;;;;;;;;;;;;;;;;;;;;;;;
(check-sat)
(get-model)

Here is what I get:

sat
(model 
  (define-fun A () (Seq Int)
    (seq.++ (seq.unit 36) (seq.++ (seq.unit (- 1)) (seq.unit 1796))))
  (define-fun m () Int
    2)
  (define-fun spec_f_A () Bool
    true)
  (define-fun f_A () (Seq Int)
    (seq.unit 74))
)

[OrenGitHub]

I've tried to make this example more minimal but couldn't.
The reason for the unsat is that (spec f_A) should be false.
When I added the assertion

(assert (= f_A (seq.unit 74)))

Then suddenly z3 answers unsat.
This suggests that something is wrong here because z3 gives f_A = (seq.unit 74)
in its model.

[OrenGitHub]

@NikolajBjorner is it safe to pull? or you guys have more fixes coming up soon? thanks!

[NikolajBjorner]

Fixing the issue with "nth" required dealing with the issue that it is only uniquely defined on indices within the bounds of the sequence. The approach for handling this is now modeled after how we deal with division and other functions that have loose interpretations. So yes I consider the issue that has to do with how "nth" gets handled internally dealt with. It took several commits.

[NikolajBjorner]

now produces unsat