summaryrefslogtreecommitdiff
path: root/tests/examples/ex67.hs
blob: ecf451c4788d5e77f4e5872552a72128337e7a2e (plain)
1
2
3
4
5
6
7
8
9
10
import Yices.Painless.Language

main = print =<< solve p

p :: Exp Int -> Exp Int -> Exp Int -> Exp Bool 
p x y z =
    (3 * x) + (6 * y) + z ==* 1
  &&*
    z ==* 2