Disable currently failing tests (#50)

* More FP regression tests

* Disable currently failing tests

regressions/smt2/6079-2.expected.out

@@ -0,0 +1 @@
+sat

regressions/smt2/6079-2.smt2

@@ -0,0 +1,6 @@
+(declare-const x Bool)
+(define-sort FPN () Float64)
+(declare-fun e () FPN)
+(declare-fun ex () FPN)
+(assert (and (= e (fp.fma roundTowardPositive e ex ex)) (= e (fp (_ bv1 1) #b11111111110 #b1111111111111111111111111111111111111111111111111111)) x))
+(check-sat)

regressions/smt2/6079-3.expected.out

@@ -0,0 +1 @@
+sat

regressions/smt2/6079-3.smt2

@@ -0,0 +1,6 @@
+(set-option :model_validate true)
+
+(declare-const a (_ FloatingPoint 11  53))
+(declare-const b (_ FloatingPoint 11  53))
+(assert (fp.eq (fp.max b b) (fp.fma RTZ b a b)))
+(check-sat)

regressions/smt2/6079-5.expected.out

@@ -0,0 +1 @@
+sat

regressions/smt2/6079-5.smt2

@@ -0,0 +1,10 @@
+(set-option :model_validate true)
+
+(set-option :rewriter.elim_and true) ;; invalid model
+;; (set-option :rewriter.flat false) ;; but this ok?
+
+(declare-const a (_ FloatingPoint 11  53))
+(declare-const b (_ FloatingPoint 11  53))
+(assert (fp.eq (fp.max b a) (fp.fma RTN a b
+(fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000))))
+(check-sat)

regressions/smt2/6079-6.expected.out

@@ -0,0 +1 @@
+sat

regressions/smt2/6079-6.smt2

@@ -0,0 +1,7 @@
+(set-option :model_validate true)
+(set-option :rewriter.flat false) ;; ok without
+
+(declare-const a (_ FloatingPoint 11  53))
+(declare-const b (_ FloatingPoint 11  53))
+(assert (fp.eq (fp.max b b) (fp.fma RTZ b b b)))
+(check-sat)

regressions/smt2/6079-7.expected.out

@@ -0,0 +1 @@
+sat

regressions/smt2/6079-7.smt2

@@ -0,0 +1,8 @@
+(set-option :model_validate true)
+
+(set-option :rewriter.ite_extra_rules true) ;; invalid model, ok without
+
+(declare-const a (_ FloatingPoint 11  53))
+(declare-const b (_ FloatingPoint 11  53))
+(assert (fp.eq (fp.max b a) (fp.fma RTZ b b b)))
+(check-sat)

regressions/smt2/6117-2.expected.out

@@ -0,0 +1 @@
+sat

regressions/smt2/6117-2.smt2

@@ -0,0 +1,12 @@
+(set-option :model_validate true)
+(set-info :status sat)
+
+(declare-fun a () Float64)
+(declare-fun b () Float64)
+(declare-fun c () Float64)
+(declare-fun d () Float64)
+(assert (= b (fp #b1 #b11110111010 #b1100001111010011101101001000011101111100101011101000)))
+(assert (= c (fp #b1 #b11100001101 #b0101011101011010100111111000100100100111110110100000)))
+(assert (= d (fp #b1 #b11111111110 #b1111111111111111111111111111111111111111111111111111)))
+(assert (= (fp.fma RTZ a b c) d))
+(check-sat)

regressions/smt2/6117-3.expected.out

@@ -0,0 +1 @@
+sat

regressions/smt2/6117-3.smt2

@@ -0,0 +1,11 @@
+(set-option :model_validate true)
+(set-info :status sat)
+
+(declare-fun x () Float64)
+(declare-fun y () Float64)
+(declare-fun z () Float64)
+(declare-fun r () Float64)
+(assert (distinct x (fp #b0 #b11111001010 #b0111110000010101111110101011010100011000011010010011)))
+(assert (distinct z (fp #b0 #b01001110111 #b0010111000000100111110110011001101010101110110011000)))
+(assert (= r (fp #b1 #b11111111110 #b1111111111111111111111111111111111111111111111111111) (fp.fma RTP x y z) r))
+(check-sat)

regressions/smt2/6548.smt2.disabled

@@ -0,0 +1,9 @@
+(set-option :model_validate true)
+(set-info :status sat)
+
+(set-logic ALL)
+(set-option :produce-models true)
+(declare-fun r () Real)
+(declare-fun f () (_ FloatingPoint 8 24))
+(assert (fp.gt f ((_ to_fp 8 24) roundNearestTiesToEven r)))
+(check-sat)

regressions/smt2/6553-2.smt2.disabled

@@ -0,0 +1,7 @@
+(set-option :model_validate true)
+(set-info :status sat)
+
+(declare-const x Real)
+(declare-fun v () RoundingMode)
+(assert (fp.gt (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)) (fp.neg ((_ to_fp 8 24) v x))))
+(check-sat)

regressions/smt2/6728-2-simp.smt2.disabled

@@ -0,0 +1,13 @@
+(set-option :model_validate true)
+(set-info :status unsat)
+
+(declare-const x (_ FloatingPoint 8 24))
+(declare-fun f ((_ FloatingPoint 8 24)) Bool)
+
+(assert (not
+	(=
+		(f (fp.add RNE x (_ +zero 8 24)))
+		(f (fp.add RNE (_ +zero 8 24) x))
+)))
+
+(check-sat)

regressions/smt2/6728-2.smt2.disabled

@@ -0,0 +1,13 @@
+(set-option :model_validate true)
+(set-info :status unsat)
+
+(set-logic ALL)
+(declare-const c RoundingMode)
+(declare-const x Float64)
+(declare-sort T 0)
+(declare-fun f (Float64) T)
+(assert (not
+	(=
+		(f (fp.add c x (_ NaN 11 53)))
+		(f (fp.add c (_ NaN 11 53) x)))))
+(check-sat)