(set-logic QF_ABV)
;(set-logic QF_BV)
(set-info :source |
--------------------------------------------------------------------
This is the famous 'Almost all Binary Searches are Broken' example.
Script 'genbprbsrch.sh' (C) 2012 Armin Biere, JKU, Linz, 2012.
Version Thu Oct 18 10:56:05 CEST 2012.
--------------------------------------------------------------------
genbprbsrch.sh 1p1
--------------------------------------------------------------------
property:             1
fixed overflow:       no
only bit-vectors:     no
strength reduction:   no
unrolled loop bodies: 1
--------------------------------------------------------------------

  int bsearch (char * a, int n, char e) {
    int l = 0, r = n;
    if (!n) return 0;               
p0: assert (l + 1 >= r);			// terminate loop check
    while (l + 1 < r) {             
      printf ("l=%d r=%d%c", l, r, 012);	// backslash not allowed
      int m = (l + r) / 2;          
p1:   assert (0 <= m);				// underflow in loop check
p2:   assert (m < n);				// overflow in loop check
      if (e < a[m]) r = m;
      else l = m;
    }                               
p3: assert (0 <= l);				// underflow at exit check
p4: assert (l < n);				// overflow at exit check
    return a[l] == e;
  }                                 

  int main (void) {
    int n = rand ();
    if (n < 0) return;
    assert (0 <= n);
    char * a = malloc (n);
    assert (a <= a + n);
    (void) bsearch (a, n, rand ());
  } 
  
  $ ./bsearch 
  l=0 r=2147483647
  l=1073741823 r=2147483647 
  Segmentation fault

--------------------------------------------------------------------
|)
(set-info :status sat)

(declare-fun zero () (_ BitVec 32))
(declare-fun one  () (_ BitVec 32))
(declare-fun two  () (_ BitVec 32))

(assert (= zero (_ bv0 32)))
(assert (= one  (_ bv1 32)))
(assert (= two  (_ bv2 32)))

(declare-fun mem () (Array (_ BitVec 64) (_ BitVec 8)))

(declare-fun n () (_ BitVec 32))
(declare-fun a () (_ BitVec 64))

(assert (bvsle zero n))					; assert (0 <= n);

(assert (bvule a (bvadd a ((_ sign_extend 32) n))))	; assert (a <= a + n);

(declare-fun e () (_ BitVec 8))

(declare-fun l0 () (_ BitVec 32))			; SSA 0th copy of l
(declare-fun r0 () (_ BitVec 32))			; SSA 0th copy of r

(assert (not (= zero n)))				; assert (!(!n));

; --------- initialization ------------------------

(assert (= l0 zero))					; l = 0;
(assert (= r0 n))					; r = n;

; --------- loop 0 --------------------------------

(assert (bvslt (bvadd l0 one) r0))			; assert (l+1 < r);
(declare-fun m0 () (_ BitVec 32))

; m = (l+r)/2; // potential overflow
(assert (= m0 (bvsdiv (bvadd l0 r0) two)))
;(assert (= m0 (bvashr (bvadd l0 r0) one)))		; strength reduction

; m = l+(r-l)/2; // no overflow
;(assert (= m0 (bvadd l0 (bvsdiv (bvsub r0 l0) two))))
;;(assert (= m0 (bvadd l0 (bvashr (bvsub r0 l0) one))))	; strength reduction

(assert (bvsle zero m0))
(assert (bvslt m0 n))
(assert (bvsle zero m0))				; assert (0 <= m);
(assert (bvslt m0 n))					; assert (m < n);

(declare-fun c0 () Bool)
(assert (= c0 (bvslt e (select mem ((_ sign_extend 32) m0)))))
(declare-fun l1 () (_ BitVec 32))
(assert (= l1 (ite c0 l0 m0)))
(declare-fun r1 () (_ BitVec 32))
(assert (= r1 (ite c0 m0 r0)))

; --------- loop 1 --------------------------------

(assert (bvslt (bvadd l1 one) r1))			; assert (l+1 < r);
(declare-fun m1 () (_ BitVec 32))

; m = (l+r)/2; // potential overflow
(assert (= m1 (bvsdiv (bvadd l1 r1) two)))
;(assert (= m1 (bvashr (bvadd l1 r1) one)))		; strength reduction

; m = l+(r-l)/2; // no overflow
;(assert (= m1 (bvadd l1 (bvsdiv (bvsub r1 l1) two))))
;;(assert (= m1 (bvadd l1 (bvashr (bvsub r1 l1) one))))	; strength reduction


; --------- property 1 --------------------------------

(assert (not (bvsle zero m1)))				; assert (!(0 <= m));

; --------------------------------------------------------------------

(check-sat)
(exit)