module SMT.Unsafe.Examples where

open import Agda.Builtin.String using (String)

open import SMT.Examples using (problem₁; problem₂; problem₄; problem₆; problem₇; problem₉)
open import SMT.Unsafe.Assume public
open import SMT.Unsafe.Z3

z3-version-output : String
z3-version-output = z3Version

z3-problem₁-output : String
z3-problem₁-output = z3CounterexampleQuery problem₁

z3-problem₂-output : String
z3-problem₂-output = z3CounterexampleQuery problem₂

z3-problem₄-output : String
z3-problem₄-output = z3CounterexampleQuery problem₄

z3-problem₆-check-output : String
z3-problem₆-check-output = z3CounterexampleCheck problem₆

z3-problem₇-output : String
z3-problem₇-output = z3CounterexampleQuery problem₇

z3-problem₉-check-output : String
z3-problem₉-check-output = z3CounterexampleCheck problem₉