Skip to content

Commit 6b79d88

Browse files
agilotvkuncak
agilot
authored and
vkuncak
committed
Disable unroll and native for FP tests
1 parent 06fbea3 commit 6b79d88

File tree

2 files changed

+69
-3
lines changed

2 files changed

+69
-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, cvc4 = true)) { ctx =>
403+
test("Floating point literals", filterSolvers(_, princess = true, cvc4 = true, native = true, unroll = 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, cvc4 = true)) { ctx =>
417+
test("Floating Point Arithmetic", filterSolvers(_, princess = true, cvc4 = true, native = true, unroll = 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, cvc4 = true)) { ctx =>
447+
test("Floating Point Comparisons", filterSolvers(_, princess = true, cvc4 = true, native = true, unroll = true)) { ctx =>
448448
val s = solver(ctx)
449449

450450

‎test.smt2‎

Lines changed: 66 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,66 @@
1+
(declare-fun |goto_symex::&92;guard#1| () Bool)
2+
(declare-fun |c::main::1::c!0@1#1| () (_ FloatingPoint 8 24))
3+
(declare-fun |c::main::1::b!0@1#1| () (_ FloatingPoint 8 24))
4+
(declare-fun |c::main::1::a!0@1#1| () (_ FloatingPoint 8 24))
5+
(define-fun _t_3 () RoundingMode RNE)
6+
(define-fun _t_9 () (_ FloatingPoint 8 24) |c::main::1::a!0@1#1|)
7+
(define-fun _t_10 () (_ FloatingPoint 11 53) ((_ to_fp 11 53) _t_3 _t_9))
8+
(define-fun _t_12 () (_ FloatingPoint 11 53) (fp #b0 #b10000000010 #b0100000000000000000000000000000000000000000000000000))
9+
(define-fun _t_13 () Bool (fp.lt _t_10 _t_12))
10+
(define-fun _t_14 () (_ FloatingPoint 8 24) |c::main::1::b!0@1#1|)
11+
(define-fun _t_15 () (_ FloatingPoint 8 24) |c::main::1::c!0@1#1|)
12+
(define-fun _t_16 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_14 _t_15))
13+
(define-fun _t_17 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_9 _t_16))
14+
(define-fun _t_18 () (_ FloatingPoint 8 24) (fp.neg _t_17))
15+
(define-fun _t_19 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_9 _t_14))
16+
(define-fun _t_20 () (_ FloatingPoint 8 24) (fp.mul _t_3 _t_15 _t_19))
17+
(define-fun _t_21 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_18 _t_20))
18+
(define-fun _t_23 () (_ FloatingPoint 8 24) (fp #b0 #b10000011 #b11100000000000000000000))
19+
(define-fun _t_24 () Bool (fp.leq _t_21 _t_23))
20+
(define-fun _t_26 () (_ FloatingPoint 11 53) (fp #b1 #b10000000010 #b0100000000000000000000000000000000000000000000000000))
21+
(define-fun _t_27 () Bool (fp.lt _t_26 _t_10))
22+
(define-fun _t_28 () Bool (and _t_13 _t_27))
23+
(define-fun _t_29 () (_ FloatingPoint 11 53) ((_ to_fp 11 53) _t_3 _t_14))
24+
(define-fun _t_30 () Bool (fp.lt _t_29 _t_12))
25+
(define-fun _t_31 () Bool (and _t_28 _t_30))
26+
(define-fun _t_32 () Bool (fp.lt _t_26 _t_29))
27+
(define-fun _t_33 () Bool (and _t_31 _t_32))
28+
(define-fun _t_34 () (_ FloatingPoint 11 53) ((_ to_fp 11 53) _t_3 _t_15))
29+
(define-fun _t_35 () Bool (fp.lt _t_34 _t_12))
30+
(define-fun _t_36 () Bool (and _t_33 _t_35))
31+
(define-fun _t_37 () Bool (fp.lt _t_26 _t_34))
32+
(define-fun _t_38 () Bool (and _t_36 _t_37))
33+
(define-fun _t_39 () Bool (fp.leq _t_14 _t_9))
34+
(define-fun _t_40 () Bool (and _t_38 _t_39))
35+
(define-fun _t_41 () Bool (fp.leq _t_15 _t_14))
36+
(define-fun _t_42 () Bool (and _t_40 _t_41))
37+
(define-fun _t_43 () (_ FloatingPoint 8 24) (fp.neg _t_14))
38+
(define-fun _t_44 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_9 _t_43))
39+
(define-fun _t_46 () (_ FloatingPoint 8 24) (fp #b0 #b01111101 #b00110011001100110011001))
40+
(define-fun _t_47 () Bool (fp.leq _t_44 _t_46))
41+
(define-fun _t_48 () Bool (and _t_42 _t_47))
42+
(define-fun _t_49 () (_ FloatingPoint 8 24) (fp.neg _t_15))
43+
(define-fun _t_50 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_9 _t_49))
44+
(define-fun _t_51 () Bool (fp.leq _t_50 _t_46))
45+
(define-fun _t_52 () Bool (and _t_48 _t_51))
46+
(define-fun _t_53 () (_ FloatingPoint 8 24) (fp.add _t_3 _t_14 _t_49))
47+
(define-fun _t_54 () Bool (fp.leq _t_53 _t_46))
48+
(define-fun _t_55 () Bool (and _t_52 _t_54))
49+
(define-fun _t_56 () (_ FloatingPoint 11 53) ((_ to_fp 11 53) _t_3 _t_20))
50+
(define-fun _t_57 () (_ FloatingPoint 11 53) (_ +oo 11 53))
51+
(define-fun _t_58 () Bool (fp.lt _t_56 _t_57))
52+
(define-fun _t_59 () (_ FloatingPoint 11 53) (_ -oo 11 53))
53+
(define-fun _t_60 () Bool (fp.lt _t_59 _t_56))
54+
(define-fun _t_61 () Bool (and _t_58 _t_60))
55+
(define-fun _t_62 () Bool (and _t_55 _t_61))
56+
(define-fun _t_63 () (_ FloatingPoint 11 53) ((_ to_fp 11 53) _t_3 _t_17))
57+
(define-fun _t_64 () Bool (fp.lt _t_63 _t_57))
58+
(define-fun _t_65 () Bool (fp.lt _t_59 _t_63))
59+
(define-fun _t_66 () Bool (and _t_64 _t_65))
60+
(define-fun _t_67 () Bool (and _t_62 _t_66))
61+
(define-fun _t_68 () Bool (fp.leq _t_17 _t_20))
62+
(define-fun _t_69 () Bool (and _t_67 _t_68))
63+
(define-fun _t_70 () Bool (not _t_24))
64+
(define-fun _t_71 () Bool (and _t_69 _t_70))
65+
(assert _t_71)
66+
(check-sat)

0 commit comments

Comments
 (0)