;;;; basic.scm ---      -*- mode: scheme; coding: utf-8; -*-
;;;;
;;;;   Copyright (C) 2020 Julien Lepiller <julien@lepiller.eu>
;;;;
;;;; This library is free software; you can redistribute it and/or
;;;; modify it under the terms of the GNU Lesser General Public
;;;; License as published by the Free Software Foundation; either
;;;; version 3 of the License, or (at your option) any later version.
;;;;
;;;; This library is distributed in the hope that it will be useful,
;;;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;;;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
;;;; Lesser General Public License for more details.
;;;;
;;;; You should have received a copy of the GNU Lesser General Public
;;;; License along with this library; if not, write to the Free Software
;;;; Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA

(define-module (tests basic-test)
  #:use-module (srfi srfi-64)
  #:use-module (ice-9 format)
  #:use-module (z3))


(test-begin "basic")

(test-assert "z3 trivial sat"
  (equal?
    (run-with-z3
      (lambda (context)
        (z3-eval context '((assert true) (check-sat)))))
    'sat))

(test-assert "z3 trivial unsat"
  (equal?
    (run-with-z3
      (lambda (context)
        (z3-eval context '((assert false) (check-sat)))))
    'unsat))

(test-end "basic")