diff options
| author | Clark Barrett <clarkbarrett@google.com> | 2015-04-23 09:43:52 -0700 |
|---|---|---|
| committer | Clark Barrett <clarkbarrett@google.com> | 2015-04-23 09:43:52 -0700 |
| commit | dea679ce032c130d210d54c2e5482f95db1ff04a (patch) | |
| tree | 6c36f68150172b20717f7d504274ab0bf82791b0 /test/regress/regress0/fmf/fc-pigeonhole19.smt2 | |
| parent | d95fe7675e20eaee86b8e804469e6db83265a005 (diff) | |
A few more minor updates to match google repository with CVC4 repository
(mostly whitespace differences).
Diffstat (limited to 'test/regress/regress0/fmf/fc-pigeonhole19.smt2')
| -rw-r--r-- | test/regress/regress0/fmf/fc-pigeonhole19.smt2 | 38 |
1 files changed, 19 insertions, 19 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 |