uni/fmi/fmi23block2/exercise2.smt2

; declare constants as 64-bit vectors
(declare-const l (_ BitVec 64))
(declare-const h (_ BitVec 64))
(declare-const m (_ BitVec 64))

;(echo "does (m = (l + h) / 2) and (0 <= l <= h) imply (l <= m <= h)?")

; declare our conjecture we want to check
(define-fun conjecture () Bool
	(=> (and (bvsle #x0000000000000000 l) (bvsle l h))
	    (and (bvsle l m) (bvsle m h))))

; constrain the values of m
; (l + h) / 2 = (l + h) >> 2
(assert (= m (bvsdiv (bvadd l h) #x0000000000000002)))

; we assert the negation of our conjecture
; if the result is sat, then a model that is a counterexample will be yielded
(assert (not conjecture))
;(echo "counterexample in the theory of 64-bitvectors: sat")

; we expect satisfiability
(check-sat)
;(get-model)

(reset)
; declaring integers this time
(declare-const l Int)
(declare-const h Int)
(declare-const m Int)

; same as above
(define-fun conjecture () Bool
	(=> (and (<= 0 l) (<= l h))
	    (and (<= l m) (<= m h))))

; constrain the values of m
(assert (= m (div (+ l h) 2)))

; again we assert the negation
(assert (not conjecture))

; this time we expect *unsatisfiability*
(check-sat)

(reset)

; repeat of 1 but with different premise
(declare-const l (_ BitVec 64))
(declare-const h (_ BitVec 64))
(declare-const m (_ BitVec 64))

(define-fun conjecture () Bool
	(=> (and (bvsle #x0000000000000000 l) (bvsle l h))
	    (and (bvsle l m) (bvsle m h))))

; constrain the values of m
; l + ((h - l) / 2) = l + ((h - l) >> 2)
(assert (= m (bvadd l (bvsdiv (bvsub h l) #x0000000000000002))))
(assert (not conjecture))

; we expect *unsatisfiability*
(check-sat)