uni/fmi/fmi23block2/exercise3.smt2

(set-option :produce-unsat-cores true)
;(set-option :produce-proofs true)

(declare-sort C)
(declare-const x C)
(declare-const y C)
(declare-const z C)
(declare-fun F (C) C)
(declare-fun G (C) C)

(push)

; we assert the entire EUF formula
(assert (! (= x y) :named A1))
(assert (! (= (F x) (G (G y))) :named A2))
(assert (! (= z (G (F y))) :named A3))
(assert (! (not (= z (G (F x)))) :named A4))

; check for satisfiability
(check-sat)
;(get-unsat-core)

(pop)

; now we define the flat symbols
(declare-const fx C)
(declare-const fy C)
(declare-const gy C)
(declare-const ggy C)
(declare-const gfx C)
(declare-const gfy C)

(push)

; this time we assert the translated formula by asserting both flat and the functional constraints

; assert flatE(phiEUF)
(assert (= x y))
(assert (= fx ggy))
(assert (= z gfy))
(assert (not (= z gfx)))

; assert FCE(phiEUF)
(assert (! (=> (= x y) (= fx fy)) :named F1))
(assert (! (=> (= y gy) (= gy ggy)) :named F2))
(assert (! (=> (= y fx) (= gy gfx)) :named F3))
(assert (! (=> (= y fy) (= gy gfy)) :named F4))
(assert (! (=> (= fx fy) (= gfx gfy)) :named F5))
(assert (! (=> (= gy fx) (= ggy gfx)) :named F6))
(assert (! (=> (= gy fy) (= ggy gfy)) :named F7))

; check for satisfiability again
(check-sat)
; extract the unsatisfiability core
(get-unsat-core)

(pop)