; COMMAND-LINE: --finite-model-find -i
; EXPECT: sat
; EXPECT: unsat
(set-logic ALL)
(set-option :incremental true)
(declare-sort prin 0)
(declare-sort form 0)
(declare-fun signed (prin form) Bool)
(declare-fun says (prin form) Bool)
(declare-fun speaksfor (prin prin) form)
(define-fun signedE () Bool (forall ((x prin) (y form)) (=> (signed x y) (says x y))))
(define-fun saysE () Bool (forall ((x prin) (y prin) (z form)) (=> (and (says x (speaksfor y x)) (says y z)) (says x z))))
(assert (forall ((x prin) (y form)) (=> (signed x y) (says x y))))
(assert (forall ((x prin) (y prin) (z form)) (=> (and (says x (speaksfor y x)) (says y z)) (says x z))))
(declare-fun julie () prin)
(declare-fun dave () prin)
(declare-fun alice () prin)
(declare-fun openfile () form)
(define-fun x2 () Bool (signed alice openfile))
(assert (signed alice openfile))
(define-fun x3 () Bool (signed dave (speaksfor alice dave)))
(assert (signed dave (speaksfor alice dave)))
(check-sat-assuming ( (not (not (says dave openfile))) ))
(check-sat-assuming ( (not (says dave openfile)) ))