module SMT.Unsafe.Assume where

open import Cubical.Foundations.Prelude

open import SMT.Core using (Statement)
open import SMT.Examples using (problem₆; problem₉)
open import SMT.Unsafe.Z3

problem₆-checked-type : Type₀
problem₆-checked-type = z3CheckedStatement problem₆

problem₆-checked-type-is-statement :
  problem₆-checked-type ≡ Statement problem₆
problem₆-checked-type-is-statement = refl

problem₉-checked-type : Type₀
problem₉-checked-type = z3CheckedStatement problem₉

problem₉-checked-type-is-statement :
  problem₉-checked-type ≡ Statement problem₉
problem₉-checked-type-is-statement = refl

postulate
  problem₆-assumption : z3CheckedStatement problem₆
  problem₉-assumption : z3CheckedStatement problem₉