Skip to content

Commit 06fbea3

Browse files
agilotvkuncak
authored andcommitted
Disable cvc4 in FP tests
1 parent facf943 commit 06fbea3

File tree

1 file changed

+3
-3
lines changed

1 file changed

+3
-3
lines changed

src/test/scala/inox/solvers/SemanticsSuite.scala

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -400,7 +400,7 @@ class SemanticsSuite extends AnyFunSuite {
400400
val doubleValues: Set[Double] = HashSet(0d, -0d, 0.1d, -6.7d, Double.NaN, Double.MinValue, Double.MinValue, Double.PositiveInfinity, Double.NegativeInfinity)
401401

402402

403-
test("Floating point literals", filterSolvers(_, princess = true)) { ctx =>
403+
test("Floating point literals", filterSolvers(_, princess = true, cvc4 = true)) { ctx =>
404404
val s = solver(ctx)
405405

406406
for (i <- floatValues) {
@@ -414,7 +414,7 @@ class SemanticsSuite extends AnyFunSuite {
414414

415415
}
416416

417-
test("Floating Point Arithmetic", filterSolvers(_, princess = true)) { ctx =>
417+
test("Floating Point Arithmetic", filterSolvers(_, princess = true, cvc4 = true)) { ctx =>
418418
val s = solver(ctx)
419419

420420
for (i <- floatValues; j <- floatValues) {
@@ -444,7 +444,7 @@ class SemanticsSuite extends AnyFunSuite {
444444

445445
}
446446

447-
test("Floating Point Comparisons", filterSolvers(_, princess = true)) { ctx =>
447+
test("Floating Point Comparisons", filterSolvers(_, princess = true, cvc4 = true)) { ctx =>
448448
val s = solver(ctx)
449449

450450

0 commit comments

Comments
 (0)