A few more minor updates to match google repository with CVC4 repository

(mostly whitespace differences).

3 files changed, 51 insertions, 51 deletions

diff --git a/test/regress/regress0/fmf/fc-pigeonhole19.smt2 b/test/regress/regress0/fmf/fc-pigeonhole19.smt2
index 15c36682c..f145013d8 100644
--- a/test/regress/regress0/fmf/fc-pigeonhole19.smt2
+++ b/test/regress/regress0/fmf/fc-pigeonhole19.smt2
@@ -1,20 +1,20 @@
-(set-logic UFC)

-(set-info :status unsat)

-

-(declare-sort P 0)

-(declare-sort H 0)

-

-(declare-fun p () P)

-(declare-fun h () H)

-

-; pigeonhole using native cardinality constraints

-(assert (fmf.card p 19))

-(assert (not (fmf.card p 18)))

-(assert (fmf.card h 18))

-(assert (not (fmf.card h 17)))

-

-; each pigeon has different holes

-(declare-fun f (P) H)

-(assert (forall ((p1 P) (p2 P)) (=> (not (= p1 p2)) (not (= (f p1) (f p2))))))

-

+(set-logic UFC)
+(set-info :status unsat)
+
+(declare-sort P 0)
+(declare-sort H 0)
+
+(declare-fun p () P)
+(declare-fun h () H)
+
+; pigeonhole using native cardinality constraints
+(assert (fmf.card p 19))
+(assert (not (fmf.card p 18)))
+(assert (fmf.card h 18))
+(assert (not (fmf.card h 17)))
+
+; each pigeon has different holes
+(declare-fun f (P) H)
+(assert (forall ((p1 P) (p2 P)) (=> (not (= p1 p2)) (not (= (f p1) (f p2))))))
+
 (check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/fmf/fc-unsat-pent.smt2 b/test/regress/regress0/fmf/fc-unsat-pent.smt2
index f1721cb04..2d4000e6e 100644
--- a/test/regress/regress0/fmf/fc-unsat-pent.smt2
+++ b/test/regress/regress0/fmf/fc-unsat-pent.smt2
@@ -1,20 +1,20 @@
-(set-logic QF_UFC)

-(set-info :status unsat)

-

-(declare-sort U 0)

-

-(declare-fun a () U)

-(declare-fun b () U)

-(declare-fun c () U)

-(declare-fun d () U)

-(declare-fun e () U)

-

-(assert (not (= a b)))

-(assert (not (= b c)))

-(assert (not (= c d)))

-(assert (not (= d e)))

-(assert (not (= e a)))

-

-(assert (fmf.card c 2))

-

+(set-logic QF_UFC)
+(set-info :status unsat)
+
+(declare-sort U 0)
+
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun d () U)
+(declare-fun e () U)
+
+(assert (not (= a b)))
+(assert (not (= b c)))
+(assert (not (= c d)))
+(assert (not (= d e)))
+(assert (not (= e a)))
+
+(assert (fmf.card c 2))
+
 (check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
index d946974ed..0d438f718 100644
--- a/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
+++ b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
@@ -1,14 +1,14 @@
-(set-logic UFC)

-(set-info :status unsat)

-

-(declare-sort U 0)

-

-(declare-fun a () U)

-(declare-fun b () U)

-(declare-fun c () U)

-

-(assert (not (fmf.card a 2)))

-

-(assert (forall ((x U)) (or (= x a) (= x b))))

-

+(set-logic UFC)
+(set-info :status unsat)
+
+(declare-sort U 0)
+
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+
+(assert (not (fmf.card a 2)))
+
+(assert (forall ((x U)) (or (= x a) (= x b))))
+
 (check-sat)
\ No newline at end of file