blob: b4a19afa813e5e88f656d8d8e4f217d42dd3a0cf (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
|
###############################################################################
# Top contributors (to current version):
# Yoni Zohar
#
# This file is part of the cvc5 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)
|
