test/regress/regress1/quantifiers/cee-os-delta.smt2


1
2
3
4
5
6
7
8
9

; COMMAND-LINE: --full-saturate-quant --ee-mode=distributed
; COMMAND-LINE: --full-saturate-quant --ee-mode=central
; EXPECT: unsat
(set-logic ALL)
(declare-fun o (Int) Int)
(declare-fun f (Int Int) Int)
(assert (forall ((x Int)) (forall ((y Int)) (! (= 1 (* y (div y y))) :pattern ((f x y))))))
(assert (= 0 (f (o 0) (o 1))))
(check-sat)