#####################
## test_solver.py
## Top contributors (to current version):
##   Yoni Zohar
## This file is part of the CVC4 project.
## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
## in the top-level source directory and their institutional affiliations.
## All rights reserved.  See the file COPYING in the top-level source
## directory for licensing information.
##
import pytest
import pycvc4
import sys

from pycvc4 import kinds

@pytest.fixture
def solver():
    return pycvc4.Solver()

def test_recoverable_exception(solver):
    solver.setOption("produce-models", "true")
    x = solver.mkConst(solver.getBooleanSort(), "x")
    solver.assertFormula(x.eqTerm(x).notTerm())
    with pytest.raises(RuntimeError):
        c = solver.getValue(x)

def test_supports_floating_point(solver):
    if solver.supportsFloatingPoint():
      try:
          solver.mkRoundingMode(pycvc4.RoundNearestTiesToEven)
      except RuntimeError:
          pytest.fail()
    else:
        with pytest.raises(RuntimeError):
          solver.mkRoundingMode(pycvc4.RoundNearestTiesToEven)