1366,768 results in assertion violation -- 1365,768 does not

assertion.txt

ASSERTION VIOLATION
File: ../src/smt/theory_arith_aux.h
Line: 1996
valid_assignment()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
A

layout.z3

;; Point(x, y)
(declare-datatypes (X Y) ((Point (makePoint (x X) (y Y)))))
(define-sort IntPoint () (Point Int Int))


;; Box(p0, p1, p2, p3)
;;
;; p3--p2
;; |   |
;; p0--p1
;;
(declare-datatypes (P0 P1 P2 P3) ((Box (makeBox (p0 P0) (p1 P1) (p2 P2) (p3 P3)))))
(define-sort IntBox () (Box IntPoint IntPoint IntPoint IntPoint))


;; Axis aligned constructor
(define-fun makeBoxFromAnchorPoints ((p0 IntPoint) (p2 IntPoint)) (IntBox)
  (makeBox p0 (makePoint (x p2) (y p0)) p2 (makePoint (x p0) (y p2))))


;; Precondition: (and (boxAxixAligned? box) (boxExpandsTopRight? box))
(define-fun boxWidth ((box IntBox)) (Int)
  (- (x (p1 box)) (x (p0 box))))

;; Precondition: (and (boxAxixAligned? box) (boxExpandsTopRight? box))
(define-fun boxHeight ((box IntBox)) (Int)
  (- (y (p3 box)) (y (p0 box))))

;; Precondition: (and (boxAxixAligned? box) (boxExpandsTopRight? box))
(define-fun boxArea ((box IntBox)) (Int)
  (* (boxWidth box) (boxHeight box)))


;; +
;; ^ 
;; |       Origin (0, 0) at bottom left, expands (i.e. not empty box)
;; ---> +
;;
(define-fun boxExpandsTopRight? ((box IntBox)) (Bool)
  (and
    (> (x (p1 box)) (x (p0 box)))
    (> (x (p2 box)) (x (p3 box)))
    (> (y (p3 box)) (y (p0 box)))
    (> (y (p2 box)) (y (p1 box)))))


;; Axis alignment for y-axis, y-axis
(define-fun boxAxisAligned? ((box IntBox)) (Bool)
  (and
    (= (x (p0 box)) (x (p3 box)))
    (= (x (p1 box)) (x (p2 box)))
    (= (y (p0 box)) (y (p1 box)))
    (= (y (p3 box)) (y (p2 box)))))


;; Precondition: (and (boxAxisAligned? b0) (boxAxisAligned? b1)
;;                    (boxExpandsTopRight? b0) (boxExpandsTopRight? b1))
(define-fun boxOverlapsBox? ((b0 IntBox) (b1 IntBox)) (Bool)
  (not (or
    (> (x (p0 b1)) (x (p1 b0)))
    (< (x (p1 b1)) (x (p0 b0)))
    (< (y (p3 b1)) (y (p0 b0)))
    (> (y (p0 b1)) (y (p3 b0))))))


;; Precondition: (and (boxAxisAligned? b0) (boxAxisAligned? b1)
;;                    (boxExpandsTopRight? b0) (boxExpandsTopRight? b1))
;; Check if b1 is inside b0
(define-fun boxInsideBox? ((b0 IntBox) (b1 IntBox)) (Bool)
  (and
    (> (x (p0 b1)) (x (p0 b0)))
    (> (y (p0 b1)) (y (p0 b0)))
    (< (x (p2 b1)) (x (p2 b0)))
    (< (y (p2 b1)) (y (p2 b0)))))




;; Environment
(define-fun laptopView () (IntBox)
  (makeBoxFromAnchorPoints (makePoint 0 0) (makePoint 1366 768)))

(define-fun phoneView () (IntBox)
  (makeBoxFromAnchorPoints (makePoint 0 0) (makePoint 768 1280)))


(declare-const box0 (IntBox))
(declare-const box1 (IntBox))


;; Constraints
(assert (and
          (boxAxisAligned? box0)
	        (boxAxisAligned? box1)

          (boxExpandsTopRight? box0)
          (boxExpandsTopRight? box1)

          ;(< 10 (boxArea box0) 25)
          ;(< 10 (boxArea box1) 25)

          (< 10 (boxWidth box0) 25)
          (< 10 (boxHeight box0) 25)

          (< 10 (boxWidth box1) 25)
          (< 10 (boxHeight box1) 25)

          (boxInsideBox? laptopView box0)
          (boxInsideBox? laptopView box1)

          ;(boxInsideBox? phoneView box0)
          ;(boxInsideBox? phoneView box1)

          (not (boxOverlapsBox? box0 box1))

          true))


(check-sat)
(get-model)

I am unable to reproduce this with latest versions of unstable (or opt)