;;;; 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")