programming-without-regret/coverageStringInsert.smt
794fd0eaba64master

coverageStringInsert.smt
View Options

			(declare-fun l () Int)

			(declare-fun r () Int)

			(declare-fun a () Int)

			(declare-fun b () Int)

			(declare-fun dirIsRight () Bool)

			(assert (< (+ l r) (+ a b)))

			(assert (not
			(or
			(or
			(or (> l a) (and (= l a) (or (< r b) dirIsRight)))
			(or (> r b) (and (= r b) (or (< l a) (not dirIsRight))))
			)
			(and (< l a) (< r b))
			)
			))

			(check-sat)

			(get-model)