diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-02-06 18:45:04 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-02-06 18:45:04 +0100 |
| commit | e8b35c4b975a46a5dc5e0c022897359cbfe2d72b (patch) | |
| tree | 63eefc37ce7964ffbfdc847dabe8e59e5894b540 /test/monniaux/picosat-965 | |
| parent | 5ad25465f77c3009eaff7e9a124c254c1e9f33cd (diff) | |
| download | compcert-kvx-e8b35c4b975a46a5dc5e0c022897359cbfe2d72b.tar.gz compcert-kvx-e8b35c4b975a46a5dc5e0c022897359cbfe2d72b.zip | |
Makefiles now use rules.mk, and added a prohibition of unprototyped functions
Diffstat (limited to 'test/monniaux/picosat-965')
| -rw-r--r-- | test/monniaux/picosat-965/picosat.c | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/test/monniaux/picosat-965/picosat.c b/test/monniaux/picosat-965/picosat.c index 2d3c96b7..31b299c0 100644 --- a/test/monniaux/picosat-965/picosat.c +++ b/test/monniaux/picosat-965/picosat.c @@ -3366,6 +3366,7 @@ report (PS * ps, int replevel, char type) { if (ps->reports >= 0) fprintf (ps->out, "%s%c ", ps->prefix, type); +#ifdef DMONNIAUX_DISABLE relem (ps, "seconds", 1, ps->seconds); relem (ps, "level", 1, avglevel (ps)); @@ -3390,6 +3391,7 @@ report (PS * ps, int replevel, char type) // relem (ps, "llused", 0, ps->llused); relem (ps, 0, 0, 0); +#endif ps->reports++; } @@ -5455,7 +5457,6 @@ simplify (PS * ps, int forced) ps->lsimplify = ps->propagations + delta; ps->fsimplify = ps->fixed; ps->simps++; - report (ps, 1, 's'); } |