\documentclass[a4paper,10pt]{article} \usepackage{a4wide} \usepackage{longtable} \usepackage{xcolor} \begin{document} \textbf{Coverage Report (Law Checking, generated 1.4.2023 23:5, commit no revision found)} \\\\ animator \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{476} & \textbf{98} & \textbf{1} & \textbf{20.6} & \textbf{206} & \textbf{62} & \textbf{0} & \textbf{30.1} \\ \hline \textcolor[HTML]{FF0000}{b\_operation\_cache.pl} & \textcolor[HTML]{FF0000}{70} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{2.9} & \textcolor[HTML]{FF0000}{37} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{5.4} \\ \hline specfile.pl & 318 & 93 & 1 & 29.3 & 126 & 57 & 0 & 45.2 \\ \hline \textcolor[HTML]{FF0000}{state\_space\_dijkstra.pl} & \textcolor[HTML]{FF0000}{13} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{10} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{xtl\_interface.pl} & \textcolor[HTML]{FF0000}{75} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{4.0} & \textcolor[HTML]{FF0000}{33} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{9.1} \\ \hline \end{longtable} ast \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{1299} & \textbf{544} & \textbf{7} & \textbf{42.1} & \textbf{615} & \textbf{295} & \textbf{0} & \textbf{48.0} \\ \hline b\_machine\_hierarchy.pl & 232 & 83 & 5 & 36.6 & 113 & 45 & 0 & 39.8 \\ \hline b\_operation\_guards.pl & 64 & 32 & 0 & 50.0 & 25 & 12 & 0 & 48.0 \\ \hline bmachine.pl & 588 & 369 & 7 & 63.5 & 326 & 217 & 0 & 66.6 \\ \hline bvisual2.pl & 415 & 60 & 0 & 14.5 & 151 & 21 & 0 & 13.9 \\ \hline \end{longtable} cbc \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{851} & \textbf{77} & \textbf{14} & \textbf{9.2} & \textbf{426} & \textbf{59} & \textbf{0} & \textbf{13.8} \\ \hline random\_permutations.pl & 9 & 9 & 0 & 100.0 & 7 & 7 & 0 & 100.0 \\ \hline \textcolor[HTML]{FF0000}{softfloat.pl} & \textcolor[HTML]{FF0000}{34} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline b\_state\_model\_check.pl & 157 & 28 & 3 & 18.2 & 83 & 22 & 0 & 26.5 \\ \hline cbc\_path\_solver.pl & 40 & 24 & 1 & 61.5 & 26 & 18 & 0 & 69.2 \\ \hline \textcolor[HTML]{FF0000}{enabling\_analysis.pl} & \textcolor[HTML]{FF0000}{131} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{3.1} & \textcolor[HTML]{FF0000}{56} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{5.4} \\ \hline \textcolor[HTML]{FF0000}{disprover.pl} & \textcolor[HTML]{FF0000}{39} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{22} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{disprover\_test\_runner.pl} & \textcolor[HTML]{FF0000}{49} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{35} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{before\_after\_predicates.pl} & \textcolor[HTML]{FF0000}{60} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{31} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{optimizing\_solver.pl} & \textcolor[HTML]{FF0000}{26} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{13} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{unsat\_cores.pl} & \textcolor[HTML]{FF0000}{119} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{63} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{weakest\_preconditions.pl} & \textcolor[HTML]{FF0000}{50} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{21} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{solver\_interface.pl} & \textcolor[HTML]{FF0000}{94} & \textcolor[HTML]{FF0000}{6} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{6.5} & \textcolor[HTML]{FF0000}{38} & \textcolor[HTML]{FF0000}{5} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{13.2} \\ \hline static\_enabling\_analysis.pl & 7 & 6 & 0 & 85.7 & 4 & 4 & 0 & 100.0 \\ \hline \textcolor[HTML]{FF0000}{cbc\_refinement\_checks.pl} & \textcolor[HTML]{FF0000}{36} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{23} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} cdclt \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{1073} & \textbf{0} & \textbf{12} & \textbf{0.0} & \textbf{411} & \textbf{0} & \textbf{0} & \textbf{0.0} \\ \hline \textcolor[HTML]{FF0000}{cdclt\_pred\_to\_sat.pl} & \textcolor[HTML]{FF0000}{106} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{39} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{cdclt\_preprocessing.pl} & \textcolor[HTML]{FF0000}{175} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{48} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{cdclt\_sat\_solver.pl} & \textcolor[HTML]{FF0000}{261} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{10} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{160} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{cdclt\_settings.pl} & \textcolor[HTML]{FF0000}{18} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{18} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{cdclt\_solver.pl} & \textcolor[HTML]{FF0000}{105} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{58} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{smt\_solver\_benchmarks.pl} & \textcolor[HTML]{FF0000}{408} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{88} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} cli \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{1965} & \textbf{295} & \textbf{18} & \textbf{15.2} & \textbf{867} & \textbf{169} & \textbf{1} & \textbf{19.5} \\ \hline \textcolor[HTML]{FF0000}{eclipse\_interface.pl} & \textcolor[HTML]{FF0000}{102} & \textcolor[HTML]{FF0000}{8} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{7.8} & \textcolor[HTML]{FF0000}{76} & \textcolor[HTML]{FF0000}{8} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{10.5} \\ \hline \textcolor[HTML]{FF0000}{prob2\_interface.pl} & \textcolor[HTML]{FF0000}{491} & \textcolor[HTML]{FF0000}{9} & \textcolor[HTML]{FF0000}{7} & \textcolor[HTML]{FF0000}{1.9} & \textcolor[HTML]{FF0000}{308} & \textcolor[HTML]{FF0000}{7} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{2.3} \\ \hline prob\_cli.pl & 1310 & 278 & 11 & 21.4 & 448 & 154 & 0 & 34.4 \\ \hline \textcolor[HTML]{FF0000}{prob\_socketserver.pl} & \textcolor[HTML]{FF0000}{62} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{35} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} coverage\_analysis \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{84} & \textbf{0} & \textbf{0} & \textbf{0.0} & \textbf{54} & \textbf{0} & \textbf{0} & \textbf{0.0} \\ \hline \textcolor[HTML]{FF0000}{coverage\_tools.pl} & \textcolor[HTML]{FF0000}{84} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{54} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} csp \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{1624} & \textbf{3} & \textbf{56} & \textbf{0.2} & \textbf{603} & \textbf{3} & \textbf{1} & \textbf{0.5} \\ \hline \textcolor[HTML]{FF0000}{csp\_basic.pl} & \textcolor[HTML]{FF0000}{5} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{5} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{csp\_sequences.pl} & \textcolor[HTML]{FF0000}{58} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{21} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{csp\_sets.pl} & \textcolor[HTML]{FF0000}{268} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{15} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{99} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{csp\_tuples.pl} & \textcolor[HTML]{FF0000}{97} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{37} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{haskell\_csp.pl} & \textcolor[HTML]{FF0000}{725} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{28} & \textcolor[HTML]{FF0000}{0.1} & \textcolor[HTML]{FF0000}{245} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.4} \\ \hline \textcolor[HTML]{FF0000}{haskell\_csp\_analyzer.pl} & \textcolor[HTML]{FF0000}{290} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{5} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{95} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{refinement\_checker.pl} & \textcolor[HTML]{FF0000}{181} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{1.1} & \textcolor[HTML]{FF0000}{101} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{2.0} \\ \hline \end{longtable} dot \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{731} & \textbf{23} & \textbf{1} & \textbf{3.2} & \textbf{400} & \textbf{16} & \textbf{0} & \textbf{4.0} \\ \hline \textcolor[HTML]{FF0000}{bvisual.pl} & \textcolor[HTML]{FF0000}{152} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{69} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{bvisual\_any\_maxsolver.pl} & \textcolor[HTML]{FF0000}{5} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{dot\_graph\_generator.pl} & \textcolor[HTML]{FF0000}{61} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{29} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{maxsolver.pl} & \textcolor[HTML]{FF0000}{38} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{24} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline reduce\_graph\_state\_space.pl & 151 & 23 & 0 & 15.2 & 99 & 16 & 0 & 16.2 \\ \hline \textcolor[HTML]{FF0000}{state\_as\_dot\_graph.pl} & \textcolor[HTML]{FF0000}{56} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{22} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{state\_custom\_dot\_graph.pl} & \textcolor[HTML]{FF0000}{59} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{25} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{state\_space\_reduction.pl} & \textcolor[HTML]{FF0000}{80} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{60} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{visualize\_graph.pl} & \textcolor[HTML]{FF0000}{129} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{69} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} experimental \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{212} & \textbf{0} & \textbf{0} & \textbf{0.0} & \textbf{130} & \textbf{0} & \textbf{0} & \textbf{0.0} \\ \hline \textcolor[HTML]{FF0000}{ltsmin.pl} & \textcolor[HTML]{FF0000}{172} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{109} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{satsolver.pl} & \textcolor[HTML]{FF0000}{40} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{21} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} external\_functions \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{2245} & \textbf{608} & \textbf{13} & \textbf{27.2} & \textbf{729} & \textbf{119} & \textbf{0} & \textbf{16.3} \\ \hline \textcolor[HTML]{FF0000}{hit\_profiler.pl} & \textcolor[HTML]{FF0000}{31} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{3.2} & \textcolor[HTML]{FF0000}{15} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{6.7} \\ \hline external\_function\_declarations.pl & 212 & 194 & 1 & 91.9 & 14 & 11 & 0 & 78.6 \\ \hline external\_functions.pl & 1394 & 294 & 12 & 21.3 & 545 & 84 & 0 & 15.4 \\ \hline \textcolor[HTML]{FF0000}{avl\_ugraphs.pl} & \textcolor[HTML]{FF0000}{6} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{6} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{xml2b.pl} & \textcolor[HTML]{FF0000}{28} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{3.6} & \textcolor[HTML]{FF0000}{10} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{10.0} \\ \hline xml\_prob.pl & 574 & 118 & 0 & 20.6 & 139 & 22 & 0 & 15.8 \\ \hline \end{longtable} infrastructure \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{3890} & \textbf{1824} & \textbf{29} & \textbf{47.2} & \textbf{959} & \textbf{381} & \textbf{6} & \textbf{40.0} \\ \hline probhash.pl & 11 & 5 & 0 & 45.5 & 9 & 4 & 0 & 44.4 \\ \hline user\_signal.pl & 13 & 10 & 0 & 76.9 & 10 & 7 & 0 & 70.0 \\ \hline \textcolor[HTML]{FF0000}{compile\_time\_flags.pl} & \textcolor[HTML]{FF0000}{9} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline debug.pl & 75 & 14 & 0 & 18.7 & 65 & 12 & 0 & 18.5 \\ \hline \textcolor[HTML]{FF0000}{debugging\_calls.pl} & \textcolor[HTML]{FF0000}{70} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{4.3} & \textcolor[HTML]{FF0000}{16} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{12.5} \\ \hline \textcolor[HTML]{FF0000}{debugging\_calls\_te.pl} & \textcolor[HTML]{FF0000}{33} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{6} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline error\_manager.pl & 342 & 135 & 8 & 40.4 & 198 & 101 & 6 & 52.6 \\ \hline eventhandling.pl & 26 & 24 & 1 & 96.0 & 9 & 8 & 0 & 88.9 \\ \hline logger.pl & 89 & 24 & 4 & 28.2 & 43 & 18 & 0 & 41.9 \\ \hline module\_information.pl & 6 & 2 & 0 & 33.3 & 6 & 2 & 0 & 33.3 \\ \hline pathes.pl & 23 & 20 & 0 & 87.0 & 18 & 17 & 0 & 94.4 \\ \hline preferences.pl & 1966 & 1316 & 0 & 66.9 & 103 & 40 & 0 & 38.8 \\ \hline prob\_startup.pl & 1 & 1 & 0 & 100.0 & 1 & 1 & 0 & 100.0 \\ \hline succeed\_max.pl & 13 & 10 & 0 & 76.9 & 9 & 7 & 0 & 77.8 \\ \hline tools.pl & 432 & 124 & 15 & 29.7 & 196 & 83 & 0 & 42.3 \\ \hline \textcolor[HTML]{FF0000}{tools\_commands.pl} & \textcolor[HTML]{FF0000}{39} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{19} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{tools\_fastread.pl} & \textcolor[HTML]{FF0000}{118} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{39} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline tools\_files.pl & 9 & 4 & 0 & 44.4 & 6 & 3 & 0 & 50.0 \\ \hline \textcolor[HTML]{FF0000}{tools\_io.pl} & \textcolor[HTML]{FF0000}{12} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{7} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline tools\_lists.pl & 28 & 19 & 0 & 67.9 & 17 & 11 & 0 & 64.7 \\ \hline \textcolor[HTML]{FF0000}{tools\_matching.pl} & \textcolor[HTML]{FF0000}{180} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.6} & \textcolor[HTML]{FF0000}{19} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{5.3} \\ \hline tools\_meta.pl & 23 & 10 & 0 & 43.5 & 16 & 6 & 0 & 37.5 \\ \hline tools\_portability.pl & 14 & 4 & 0 & 28.6 & 10 & 4 & 0 & 40.0 \\ \hline tools\_positions.pl & 23 & 5 & 0 & 21.7 & 5 & 2 & 0 & 40.0 \\ \hline tools\_printing.pl & 214 & 38 & 0 & 17.8 & 65 & 17 & 0 & 26.2 \\ \hline tools\_strings.pl & 98 & 45 & 0 & 45.9 & 45 & 25 & 0 & 55.6 \\ \hline tools\_timeout.pl & 7 & 4 & 0 & 57.1 & 5 & 4 & 0 & 80.0 \\ \hline \textcolor[HTML]{FF0000}{user\_interrupts.pl} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline version.pl & 12 & 6 & 0 & 50.0 & 9 & 6 & 0 & 66.7 \\ \hline \end{longtable} \textbf{interpreter }\begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{2156} & \textbf{1398} & \textbf{33} & \textbf{65.9} & \textbf{901} & \textbf{658} & \textbf{0} & \textbf{73.0} \\ \hline b\_compiler.pl & 261 & 165 & 0 & 63.2 & 72 & 47 & 0 & 65.3 \\ \hline b\_enumerate.pl & 121 & 104 & 3 & 88.1 & 52 & 50 & 0 & 96.2 \\ \hline b\_interpreter.pl & 688 & 506 & 13 & 75.0 & 331 & 281 & 0 & 84.9 \\ \hline b\_interpreter\_check.pl & 455 & 369 & 8 & 82.6 & 122 & 114 & 0 & 93.4 \\ \hline b\_interpreter\_components.pl & 95 & 73 & 0 & 76.8 & 69 & 55 & 0 & 79.7 \\ \hline b\_interpreter\_eventb.pl & 79 & 48 & 2 & 62.3 & 52 & 36 & 0 & 69.2 \\ \hline store.pl & 210 & 115 & 7 & 56.7 & 81 & 63 & 0 & 77.8 \\ \hline \textcolor[HTML]{FF0000}{value\_persistance.pl} & \textcolor[HTML]{FF0000}{247} & \textcolor[HTML]{FF0000}{18} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{7.3} & \textcolor[HTML]{FF0000}{122} & \textcolor[HTML]{FF0000}{12} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{9.8} \\ \hline \end{longtable} \textbf{kernel }\begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{6846} & \textbf{4792} & \textbf{115} & \textbf{71.2} & \textbf{3089} & \textbf{2418} & \textbf{3} & \textbf{78.4} \\ \hline avl\_tools.pl & 47 & 34 & 4 & 79.1 & 27 & 21 & 0 & 77.8 \\ \hline b\_global\_sets.pl & 268 & 172 & 5 & 65.4 & 136 & 109 & 0 & 80.1 \\ \hline bool\_pred.pl & 29 & 22 & 0 & 75.9 & 21 & 16 & 0 & 76.2 \\ \hline bsets\_clp.pl & 768 & 575 & 7 & 75.6 & 390 & 315 & 0 & 80.8 \\ \hline chr\_integer\_inequality.pl & 460 & 258 & 0 & 56.1 & 257 & 177 & 0 & 68.9 \\ \hline chr\_set\_membership.pl & 144 & 44 & 0 & 30.6 & 88 & 29 & 0 & 33.0 \\ \hline closures.pl & 121 & 76 & 2 & 63.9 & 55 & 49 & 0 & 89.1 \\ \hline clpfd\_interface.pl & 187 & 131 & 2 & 70.8 & 102 & 83 & 0 & 81.4 \\ \hline clpfd\_lists.pl & 124 & 65 & 8 & 56.0 & 37 & 26 & 0 & 70.3 \\ \hline clpfd\_tables.pl & 47 & 39 & 0 & 83.0 & 24 & 22 & 0 & 91.7 \\ \hline custom\_explicit\_sets.pl & 1512 & 1180 & 38 & 80.1 & 608 & 550 & 0 & 90.5 \\ \hline delay.pl & 29 & 26 & 0 & 89.7 & 19 & 16 & 0 & 84.2 \\ \hline fd\_utils\_clpfd.pl & 12 & 7 & 0 & 58.3 & 9 & 7 & 0 & 77.8 \\ \hline inf\_arith.pl & 51 & 40 & 0 & 78.4 & 21 & 17 & 0 & 81.0 \\ \hline kernel\_cardinality\_attr.pl & 49 & 38 & 0 & 77.6 & 25 & 19 & 0 & 76.0 \\ \hline kernel\_dif.pl & 11 & 10 & 0 & 90.9 & 5 & 5 & 0 & 100.0 \\ \hline kernel\_equality.pl & 199 & 175 & 5 & 90.2 & 90 & 84 & 0 & 93.3 \\ \hline kernel\_frozen\_info.pl & 17 & 6 & 0 & 35.3 & 6 & 4 & 0 & 66.7 \\ \hline kernel\_lists.pl & 4 & 2 & 1 & 66.7 & 2 & 2 & 0 & 100.0 \\ \hline kernel\_mappings.pl & 459 & 382 & 0 & 83.2 & 101 & 95 & 0 & 94.1 \\ \hline kernel\_non\_empty\_attr.pl & 11 & 9 & 0 & 81.8 & 6 & 5 & 0 & 83.3 \\ \hline kernel\_objects.pl & 1225 & 878 & 11 & 72.3 & 573 & 454 & 1 & 79.4 \\ \hline \textcolor[HTML]{FF0000}{kernel\_ordering.pl} & \textcolor[HTML]{FF0000}{41} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{4.9} & \textcolor[HTML]{FF0000}{15} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{13.3} \\ \hline kernel\_propagation.pl & 4 & 4 & 0 & 100.0 & 3 & 3 & 0 & 100.0 \\ \hline \textcolor[HTML]{FF0000}{kernel\_reals.pl} & \textcolor[HTML]{FF0000}{47} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{43} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline kernel\_records.pl & 25 & 11 & 3 & 50.0 & 18 & 8 & 0 & 44.4 \\ \hline kernel\_strings.pl & 195 & 128 & 2 & 66.3 & 97 & 82 & 0 & 84.5 \\ \hline kernel\_tools.pl & 311 & 243 & 6 & 79.7 & 54 & 49 & 0 & 90.7 \\ \hline kernel\_waitflags.pl & 331 & 172 & 25 & 56.2 & 190 & 129 & 2 & 68.6 \\ \hline memoization.pl & 94 & 57 & 0 & 60.6 & 54 & 36 & 0 & 66.7 \\ \hline static\_symmetry\_reduction.pl & 24 & 6 & 0 & 25.0 & 13 & 4 & 0 & 30.8 \\ \hline \end{longtable} kodkod \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{1097} & \textbf{712} & \textbf{2} & \textbf{65.0} & \textbf{447} & \textbf{324} & \textbf{0} & \textbf{72.5} \\ \hline interval\_calc.pl & 8 & 7 & 0 & 87.5 & 6 & 5 & 0 & 83.3 \\ \hline kodkod.pl & 73 & 37 & 0 & 50.7 & 35 & 28 & 0 & 80.0 \\ \hline kodkod2.pl & 67 & 61 & 0 & 91.0 & 38 & 37 & 0 & 97.4 \\ \hline \textcolor[HTML]{FF0000}{kodkod\_annotator.pl} & \textcolor[HTML]{FF0000}{31} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{8} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline kodkod\_integer\_recalc.pl & 23 & 9 & 0 & 39.1 & 8 & 5 & 0 & 62.5 \\ \hline kodkod\_printer.pl & 121 & 104 & 0 & 86.0 & 43 & 41 & 0 & 95.3 \\ \hline kodkod\_process.pl & 68 & 42 & 2 & 63.6 & 44 & 35 & 0 & 79.5 \\ \hline kodkod\_rewrite.pl & 28 & 14 & 0 & 50.0 & 11 & 8 & 0 & 72.7 \\ \hline \textcolor[HTML]{FF0000}{kodkod\_test.pl} & \textcolor[HTML]{FF0000}{50} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{39} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline kodkod\_tools.pl & 27 & 25 & 0 & 92.6 & 18 & 18 & 0 & 100.0 \\ \hline kodkod\_translate.pl & 163 & 123 & 0 & 75.5 & 48 & 43 & 0 & 89.6 \\ \hline kodkod\_typing.pl & 83 & 68 & 0 & 81.9 & 25 & 25 & 0 & 100.0 \\ \hline predicate\_analysis.pl & 355 & 222 & 0 & 62.5 & 124 & 79 & 0 & 63.7 \\ \hline \end{longtable} ltl \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{1021} & \textbf{31} & \textbf{28} & \textbf{3.1} & \textbf{407} & \textbf{15} & \textbf{0} & \textbf{3.7} \\ \hline \textcolor[HTML]{FF0000}{ltl2ba.pl} & \textcolor[HTML]{FF0000}{5} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{5} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{ltlc.pl} & \textcolor[HTML]{FF0000}{93} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{31} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{ctl.pl} & \textcolor[HTML]{FF0000}{82} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{1.3} & \textcolor[HTML]{FF0000}{36} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{2.8} \\ \hline \textcolor[HTML]{FF0000}{ltl.pl} & \textcolor[HTML]{FF0000}{132} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{5} & \textcolor[HTML]{FF0000}{3.1} & \textcolor[HTML]{FF0000}{74} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{5.4} \\ \hline \textcolor[HTML]{FF0000}{ltl\_fairness.pl} & \textcolor[HTML]{FF0000}{56} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{31} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{ltl\_propositions.pl} & \textcolor[HTML]{FF0000}{105} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{36} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{ltl\_safety.pl} & \textcolor[HTML]{FF0000}{131} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{33} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{ltl\_tools.pl} & \textcolor[HTML]{FF0000}{165} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{7} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{65} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{ltl\_translate.pl} & \textcolor[HTML]{FF0000}{90} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{14} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline ltl\_verification.pl & 75 & 26 & 0 & 34.7 & 33 & 10 & 0 & 30.3 \\ \hline \textcolor[HTML]{FF0000}{safety\_mc.pl} & \textcolor[HTML]{FF0000}{64} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{34} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{state\_space\_explorer.pl} & \textcolor[HTML]{FF0000}{10} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{6} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{trace\_generator.pl} & \textcolor[HTML]{FF0000}{13} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{9} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} misc \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{460} & \textbf{43} & \textbf{1} & \textbf{9.4} & \textbf{179} & \textbf{31} & \textbf{0} & \textbf{17.3} \\ \hline \textcolor[HTML]{FF0000}{b\_show\_history.pl} & \textcolor[HTML]{FF0000}{40} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{23} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{coverage\_statistics.pl} & \textcolor[HTML]{FF0000}{109} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{48} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{predicate\_debugger.pl} & \textcolor[HTML]{FF0000}{54} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{36} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline predicate\_evaluator.pl & 92 & 43 & 1 & 47.3 & 51 & 31 & 0 & 60.8 \\ \hline \textcolor[HTML]{FF0000}{subtree\_compare.pl} & \textcolor[HTML]{FF0000}{165} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{21} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} model\_checker \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{395} & \textbf{37} & \textbf{2} & \textbf{9.4} & \textbf{220} & \textbf{22} & \textbf{0} & \textbf{10.0} \\ \hline model\_checker.pl & 50 & 33 & 0 & 66.0 & 21 & 18 & 0 & 85.7 \\ \hline \textcolor[HTML]{FF0000}{pge\_algo.pl} & \textcolor[HTML]{FF0000}{62} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{1.6} & \textcolor[HTML]{FF0000}{41} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{2.4} \\ \hline \textcolor[HTML]{FF0000}{ample\_sets.pl} & \textcolor[HTML]{FF0000}{79} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{3.8} & \textcolor[HTML]{FF0000}{61} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{4.9} \\ \hline \textcolor[HTML]{FF0000}{b\_simplifier.pl} & \textcolor[HTML]{FF0000}{90} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{24} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{dot\_graphs\_static\_analysis.pl} & \textcolor[HTML]{FF0000}{9} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{9} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{enable\_graph.pl} & \textcolor[HTML]{FF0000}{31} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{19} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{enabling\_predicates.pl} & \textcolor[HTML]{FF0000}{31} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{16} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{static\_analysis.pl} & \textcolor[HTML]{FF0000}{43} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{29} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} other \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{2489} & \textbf{104} & \textbf{7} & \textbf{4.2} & \textbf{909} & \textbf{40} & \textbf{1} & \textbf{4.4} \\ \hline \textcolor[HTML]{FF0000}{bliss\_interface.pl} & \textcolor[HTML]{FF0000}{28} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{19} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline counter.pl & 10 & 8 & 0 & 80.0 & 5 & 4 & 0 & 80.0 \\ \hline \textcolor[HTML]{FF0000}{ltsmin\_c\_interface.pl} & \textcolor[HTML]{FF0000}{14} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{ltsmin\_trace.pl} & \textcolor[HTML]{FF0000}{16} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{12} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{msg\_interop.pl} & \textcolor[HTML]{FF0000}{42} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{17} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline myheap.pl & 30 & 17 & 0 & 56.7 & 13 & 4 & 0 & 30.8 \\ \hline plspec.pl & 49 & 10 & 0 & 20.4 & 31 & 10 & 0 & 32.3 \\ \hline plspec\_core.pl & 14 & 12 & 0 & 85.7 & 6 & 4 & 0 & 66.7 \\ \hline plspec\_logger.pl & 18 & 3 & 0 & 16.7 & 8 & 2 & 0 & 25.0 \\ \hline \textcolor[HTML]{FF0000}{prettyprinter.pl} & \textcolor[HTML]{FF0000}{31} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{9} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{validator.pl} & \textcolor[HTML]{FF0000}{58} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{6.9} & \textcolor[HTML]{FF0000}{26} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{3.8} \\ \hline \textcolor[HTML]{FF0000}{regexp.pl} & \textcolor[HTML]{FF0000}{35} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{17} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline b\_to\_cnf.pl & 22 & 2 & 2 & 10.0 & 6 & 1 & 0 & 16.7 \\ \hline \textcolor[HTML]{FF0000}{alloy2b.pl} & \textcolor[HTML]{FF0000}{682} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{188} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline b\_arithmetic\_expressions.pl & 8 & 7 & 0 & 87.5 & 3 & 3 & 0 & 100.0 \\ \hline \textcolor[HTML]{FF0000}{ast\_to\_difference\_logic.pl} & \textcolor[HTML]{FF0000}{64} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{14} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{difference\_logic\_solver.pl} & \textcolor[HTML]{FF0000}{120} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{53} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{sat\_symmetry\_breaking.pl} & \textcolor[HTML]{FF0000}{50} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{25} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{smt\_symmetry\_breaking.pl} & \textcolor[HTML]{FF0000}{128} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{48} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{unique\_quantified\_identifiers.pl} & \textcolor[HTML]{FF0000}{45} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{13} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{code2vec.pl} & \textcolor[HTML]{FF0000}{28} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{14} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{coverage\_tools\_annotations.pl} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{external\_functions\_reals.pl} & \textcolor[HTML]{FF0000}{78} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{78} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{external\_functions\_svg.pl} & \textcolor[HTML]{FF0000}{22} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{15} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{json\_parser.pl} & \textcolor[HTML]{FF0000}{108} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{41} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline pathes\_extensions\_db.pl & 262 & 36 & 0 & 13.7 & 11 & 6 & 0 & 54.5 \\ \hline \textcolor[HTML]{FF0000}{ground\_truth.pl} & \textcolor[HTML]{FF0000}{100} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{30} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{predicate\_data\_generator.pl} & \textcolor[HTML]{FF0000}{69} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{28} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{logging.pl} & \textcolor[HTML]{FF0000}{41} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{9} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{synthesis\_util.pl} & \textcolor[HTML]{FF0000}{280} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{139} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{test\_typechecker.pl} & \textcolor[HTML]{FF0000}{25} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{16} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline prob\_cov\_runner.pl & 2 & 1 & 0 & 50.0 & 2 & 1 & 0 & 50.0 \\ \hline \textcolor[HTML]{FF0000}{alloy2b\_benchmarks.pl} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline test\_paths.pl & 5 & 4 & 0 & 80.0 & 5 & 4 & 0 & 80.0 \\ \hline \end{longtable} pltables \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{176} & \textbf{0} & \textbf{0} & \textbf{0.0} & \textbf{99} & \textbf{0} & \textbf{0} & \textbf{0.0} \\ \hline \textcolor[HTML]{FF0000}{table\_tools.pl} & \textcolor[HTML]{FF0000}{92} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{39} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{pltables.pl} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{pltables\_export.pl} & \textcolor[HTML]{FF0000}{20} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{16} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{pltables\_export\_csv.pl} & \textcolor[HTML]{FF0000}{13} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{10} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{pltables\_export\_html.pl} & \textcolor[HTML]{FF0000}{11} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{8} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{pltables\_export\_latex.pl} & \textcolor[HTML]{FF0000}{21} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{11} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{pltables\_export\_tools.pl} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{pltables\_export\_xml.pl} & \textcolor[HTML]{FF0000}{13} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{10} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} profiling \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{49} & \textbf{15} & \textbf{0} & \textbf{30.6} & \textbf{37} & \textbf{10} & \textbf{0} & \textbf{27.0} \\ \hline performance\_messages.pl & 24 & 10 & 0 & 41.7 & 14 & 6 & 0 & 42.9 \\ \hline runtime\_profiler.pl & 19 & 4 & 0 & 21.1 & 17 & 3 & 0 & 17.6 \\ \hline source\_profiler.pl & 6 & 1 & 0 & 16.7 & 6 & 1 & 0 & 16.7 \\ \hline \end{longtable} proz \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{1355} & \textbf{969} & \textbf{0} & \textbf{71.5} & \textbf{466} & \textbf{350} & \textbf{0} & \textbf{75.1} \\ \hline kernel\_freetypes.pl & 69 & 44 & 0 & 63.8 & 40 & 28 & 0 & 70.0 \\ \hline kernel\_z.pl & 19 & 16 & 0 & 84.2 & 13 & 12 & 0 & 92.3 \\ \hline consistencycheck.pl & 125 & 94 & 0 & 75.2 & 16 & 14 & 0 & 87.5 \\ \hline dependence.pl & 31 & 18 & 0 & 58.1 & 6 & 6 & 0 & 100.0 \\ \hline fuzzfile.pl & 45 & 44 & 0 & 97.8 & 25 & 24 & 0 & 96.0 \\ \hline proz.pl & 293 & 210 & 0 & 71.7 & 113 & 82 & 0 & 72.6 \\ \hline schemaexpansion.pl & 92 & 30 & 0 & 32.6 & 40 & 16 & 0 & 40.0 \\ \hline \textcolor[HTML]{FF0000}{schemavars.pl} & \textcolor[HTML]{FF0000}{23} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{8.7} & \textcolor[HTML]{FF0000}{6} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{33.3} \\ \hline subexpressions.pl & 186 & 142 & 0 & 76.3 & 48 & 39 & 0 & 81.3 \\ \hline z\_tools.pl & 32 & 17 & 0 & 53.1 & 20 & 11 & 0 & 55.0 \\ \hline z\_typechecker.pl & 264 & 200 & 0 & 75.8 & 64 & 47 & 0 & 73.4 \\ \hline zenvironment.pl & 11 & 10 & 0 & 90.9 & 7 & 7 & 0 & 100.0 \\ \hline zparameters.pl & 9 & 1 & 0 & 11.1 & 3 & 1 & 0 & 33.3 \\ \hline ztransformations.pl & 156 & 141 & 0 & 90.4 & 65 & 61 & 0 & 93.8 \\ \hline \end{longtable} repl \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{472} & \textbf{150} & \textbf{3} & \textbf{32.0} & \textbf{197} & \textbf{57} & \textbf{0} & \textbf{28.9} \\ \hline \textcolor[HTML]{FF0000}{eval\_interface.pl} & \textcolor[HTML]{FF0000}{8} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{5} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline eval\_strings.pl & 464 & 150 & 3 & 32.5 & 192 & 57 & 0 & 29.7 \\ \hline \end{longtable} smt\_solvers \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{919} & \textbf{2} & \textbf{18} & \textbf{0.2} & \textbf{290} & \textbf{2} & \textbf{0} & \textbf{0.7} \\ \hline \textcolor[HTML]{FF0000}{cvc4interface.pl} & \textcolor[HTML]{FF0000}{44} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{19} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{z3interface.pl} & \textcolor[HTML]{FF0000}{63} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{6} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{atelierb\_provers\_interface.pl} & \textcolor[HTML]{FF0000}{22} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{16} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{ast\_cleanup\_for\_smt.pl} & \textcolor[HTML]{FF0000}{112} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{33} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{ast\_optimizer\_for\_smt.pl} & \textcolor[HTML]{FF0000}{113} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{36} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{model\_translation.pl} & \textcolor[HTML]{FF0000}{219} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{5} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{77} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{prob\_state\_predicates.pl} & \textcolor[HTML]{FF0000}{19} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{5} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{seq\_rewriter.pl} & \textcolor[HTML]{FF0000}{37} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{12} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{smt\_common\_predicates.pl} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{smt\_solvers\_interface.pl} & \textcolor[HTML]{FF0000}{274} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{11} & \textcolor[HTML]{FF0000}{0.8} & \textcolor[HTML]{FF0000}{78} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{2.6} \\ \hline \textcolor[HTML]{FF0000}{solver\_dispatcher.pl} & \textcolor[HTML]{FF0000}{15} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{7} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} smtlib \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{309} & \textbf{0} & \textbf{0} & \textbf{0.0} & \textbf{107} & \textbf{0} & \textbf{0} & \textbf{0.0} \\ \hline \textcolor[HTML]{FF0000}{smtlib2\_cli.pl} & \textcolor[HTML]{FF0000}{8} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{6} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{smtlib2\_environment.pl} & \textcolor[HTML]{FF0000}{19} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{14} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{smtlib2\_interpreter.pl} & \textcolor[HTML]{FF0000}{55} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{17} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{smtlib2\_parser.pl} & \textcolor[HTML]{FF0000}{118} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{45} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{smtlib2\_translation.pl} & \textcolor[HTML]{FF0000}{109} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{25} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} state\_space \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{459} & \textbf{160} & \textbf{9} & \textbf{35.6} & \textbf{264} & \textbf{108} & \textbf{0} & \textbf{40.9} \\ \hline hashing.pl & 4 & 3 & 0 & 75.0 & 4 & 3 & 0 & 75.0 \\ \hline state\_packing.pl & 144 & 59 & 6 & 42.8 & 55 & 24 & 0 & 43.6 \\ \hline state\_space.pl & 206 & 64 & 0 & 31.1 & 149 & 55 & 0 & 36.9 \\ \hline state\_space\_exploration\_modes.pl & 74 & 21 & 0 & 28.4 & 34 & 16 & 0 & 47.1 \\ \hline state\_space\_open\_nodes\_c.pl & 31 & 13 & 3 & 46.4 & 22 & 10 & 0 & 45.5 \\ \hline \end{longtable} symbolic\_model\_checker \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{286} & \textbf{0} & \textbf{1} & \textbf{0.0} & \textbf{180} & \textbf{0} & \textbf{0} & \textbf{0.0} \\ \hline \textcolor[HTML]{FF0000}{bmc.pl} & \textcolor[HTML]{FF0000}{23} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{14} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{ce\_replay.pl} & \textcolor[HTML]{FF0000}{5} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{ctigar.pl} & \textcolor[HTML]{FF0000}{52} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{34} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{ic3.pl} & \textcolor[HTML]{FF0000}{55} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{36} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{kinduction.pl} & \textcolor[HTML]{FF0000}{32} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{19} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{mic\_generation.pl} & \textcolor[HTML]{FF0000}{20} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{10} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{predicate\_abstraction.pl} & \textcolor[HTML]{FF0000}{15} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{8} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{predicate\_handling.pl} & \textcolor[HTML]{FF0000}{55} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{37} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{solver\_handling.pl} & \textcolor[HTML]{FF0000}{26} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{17} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{unsat\_core\_generalization.pl} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} symmetry \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{225} & \textbf{16} & \textbf{1} & \textbf{7.1} & \textbf{88} & \textbf{6} & \textbf{0} & \textbf{6.8} \\ \hline \textcolor[HTML]{FF0000}{graphiso.pl} & \textcolor[HTML]{FF0000}{10} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{state\_graph\_canon.pl} & \textcolor[HTML]{FF0000}{36} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{18} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{graph\_iso\_nauty.pl} & \textcolor[HTML]{FF0000}{49} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{4.1} & \textcolor[HTML]{FF0000}{25} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{8.0} \\ \hline \textcolor[HTML]{FF0000}{state\_permuter.pl} & \textcolor[HTML]{FF0000}{32} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{10} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline symmetry\_marker.pl & 98 & 14 & 1 & 14.4 & 31 & 4 & 0 & 12.9 \\ \hline \end{longtable} synthesis \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{854} & \textbf{0} & \textbf{0} & \textbf{0.0} & \textbf{282} & \textbf{0} & \textbf{0} & \textbf{0.0} \\ \hline \textcolor[HTML]{FF0000}{b\_synthesis.pl} & \textcolor[HTML]{FF0000}{118} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{59} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{constraints.pl} & \textcolor[HTML]{FF0000}{239} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{100} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{b\_machine\_identifier\_normalization.pl} & \textcolor[HTML]{FF0000}{257} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{38} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{operation\_data\_generator.pl} & \textcolor[HTML]{FF0000}{42} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{22} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{library\_setup.pl} & \textcolor[HTML]{FF0000}{130} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{31} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{location\_vars\_to\_program.pl} & \textcolor[HTML]{FF0000}{27} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{9} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{symmetry\_reduction.pl} & \textcolor[HTML]{FF0000}{41} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{23} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} tcltk \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{578} & \textbf{61} & \textbf{0} & \textbf{10.6} & \textbf{371} & \textbf{47} & \textbf{1} & \textbf{12.7} \\ \hline tcltk\_interface.pl & 578 & 61 & 5 & 10.6 & 371 & 47 & 1 & 12.7 \\ \hline \end{longtable} test\_generation \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{378} & \textbf{83} & \textbf{2} & \textbf{22.1} & \textbf{234} & \textbf{67} & \textbf{0} & \textbf{28.6} \\ \hline sap.pl & 307 & 83 & 4 & 27.4 & 207 & 67 & 0 & 32.4 \\ \hline \textcolor[HTML]{FF0000}{mcdc\_coverage.pl} & \textcolor[HTML]{FF0000}{71} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{27} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} testing \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{3551} & \textbf{2573} & \textbf{4} & \textbf{72.5} & \textbf{481} & \textbf{109} & \textbf{0} & \textbf{22.7} \\ \hline \textcolor[HTML]{FF0000}{b\_intelligent\_trace\_replay.pl} & \textcolor[HTML]{FF0000}{172} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{103} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline b\_trace\_checking.pl & 159 & 45 & 2 & 28.7 & 74 & 29 & 0 & 39.2 \\ \hline junit\_tests.pl & 29 & 21 & 2 & 77.8 & 17 & 16 & 0 & 94.1 \\ \hline self\_check.pl & 103 & 13 & 0 & 12.6 & 80 & 13 & 0 & 16.3 \\ \hline typechecker.pl & 124 & 19 & 0 & 15.3 & 26 & 5 & 0 & 19.2 \\ \hline test\_runner.pl & 383 & 63 & 0 & 16.4 & 172 & 39 & 0 & 22.7 \\ \hline testcases.pl & 2581 & 2412 & 0 & 93.5 & 9 & 7 & 0 & 77.8 \\ \hline \end{longtable} tools \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{2275} & \textbf{719} & \textbf{18} & \textbf{31.9} & \textbf{656} & \textbf{317} & \textbf{0} & \textbf{48.3} \\ \hline gensym.pl & 10 & 8 & 0 & 80.0 & 8 & 6 & 0 & 75.0 \\ \hline pref\_definitions.pl & 38 & 18 & 0 & 47.4 & 17 & 11 & 0 & 64.7 \\ \hline \textcolor[HTML]{FF0000}{static\_ordering.pl} & \textcolor[HTML]{FF0000}{15} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{8} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline system\_call.pl & 15 & 9 & 1 & 64.3 & 14 & 9 & 0 & 64.3 \\ \hline translate.pl & 2052 & 683 & 16 & 33.5 & 602 & 290 & 0 & 48.2 \\ \hline \textcolor[HTML]{FF0000}{translate\_keywords.pl} & \textcolor[HTML]{FF0000}{145} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.7} & \textcolor[HTML]{FF0000}{7} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{14.3} \\ \hline \end{longtable} typechecker \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{5340} & \textbf{2960} & \textbf{78} & \textbf{56.3} & \textbf{2194} & \textbf{1427} & \textbf{0} & \textbf{65.0} \\ \hline b\_ast\_cleanup.pl & 918 & 658 & 3 & 71.9 & 290 & 229 & 0 & 79.0 \\ \hline b\_enumeration\_order\_analysis.pl & 68 & 45 & 1 & 67.2 & 22 & 21 & 0 & 95.5 \\ \hline b\_read\_write\_info.pl & 198 & 101 & 2 & 51.5 & 97 & 58 & 0 & 59.8 \\ \hline bmachine\_construction.pl & 563 & 326 & 12 & 59.2 & 328 & 227 & 0 & 69.2 \\ \hline bmachine\_eventb.pl & 560 & 301 & 4 & 54.1 & 292 & 221 & 0 & 75.7 \\ \hline bmachine\_static\_checks.pl & 83 & 31 & 0 & 37.3 & 46 & 23 & 0 & 50.0 \\ \hline bmachine\_structure.pl & 34 & 24 & 2 & 75.0 & 22 & 17 & 0 & 77.3 \\ \hline bsyntaxtree.pl & 1075 & 663 & 32 & 63.6 & 377 & 263 & 0 & 69.8 \\ \hline bsyntaxtree\_quantifiers.pl & 9 & 9 & 0 & 100.0 & 8 & 8 & 0 & 100.0 \\ \hline btypechecker.pl & 806 & 501 & 6 & 62.6 & 262 & 180 & 0 & 68.7 \\ \hline \textcolor[HTML]{FF0000}{b\_expression\_sharing.pl} & \textcolor[HTML]{FF0000}{346} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{7} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{126} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline input\_syntax\_tree.pl & 55 & 32 & 1 & 59.3 & 21 & 14 & 0 & 66.7 \\ \hline parsercall.pl & 275 & 101 & 9 & 38.0 & 153 & 74 & 0 & 48.4 \\ \hline partition\_detection.pl & 28 & 26 & 0 & 92.9 & 17 & 17 & 0 & 100.0 \\ \hline pathes\_lib.pl & 29 & 8 & 0 & 27.6 & 16 & 6 & 0 & 37.5 \\ \hline pragmas.pl & 10 & 4 & 0 & 40.0 & 5 & 4 & 0 & 80.0 \\ \hline record\_detection.pl & 98 & 39 & 1 & 40.2 & 69 & 31 & 0 & 44.9 \\ \hline b\_ast\_cleanup\_rewrite\_rules.pl & 29 & 17 & 0 & 58.6 & 13 & 13 & 0 & 100.0 \\ \hline rewrite\_rules\_db.pl & 27 & 16 & 0 & 59.3 & 2 & 2 & 0 & 100.0 \\ \hline typing\_tools.pl & 129 & 58 & 1 & 45.3 & 28 & 19 & 0 & 67.9 \\ \hline \end{longtable} visualization \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{962} & \textbf{2} & \textbf{4} & \textbf{0.2} & \textbf{353} & \textbf{2} & \textbf{0} & \textbf{0.6} \\ \hline \textcolor[HTML]{FF0000}{graphical\_state\_viewer\_images.pl} & \textcolor[HTML]{FF0000}{148} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{83} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{latex\_processor.pl} & \textcolor[HTML]{FF0000}{111} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{49} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{meta\_interface.pl} & \textcolor[HTML]{FF0000}{365} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{41} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{visb\_visualiser.pl} & \textcolor[HTML]{FF0000}{338} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.6} & \textcolor[HTML]{FF0000}{180} & \textcolor[HTML]{FF0000}{2} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1.1} \\ \hline \end{longtable} well\_def\_prover \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{1679} & \textbf{0} & \textbf{15} & \textbf{0.0} & \textbf{337} & \textbf{0} & \textbf{0} & \textbf{0.0} \\ \hline \textcolor[HTML]{FF0000}{well\_def\_analyser.pl} & \textcolor[HTML]{FF0000}{335} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{90} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{well\_def\_hyps.pl} & \textcolor[HTML]{FF0000}{210} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{14} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{62} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{well\_def\_prover.pl} & \textcolor[HTML]{FF0000}{972} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{1} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{174} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{well\_def\_tools.pl} & \textcolor[HTML]{FF0000}{162} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{11} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} zmq \begin{longtable}{|l|r|r|r|r|r|r|r|r|} \hline module & clauses & covered & uncoverable & \% & preds & covered & uncoverable & \% \\ \hline \textbf{summary} & \textbf{49} & \textbf{0} & \textbf{0} & \textbf{0.0} & \textbf{27} & \textbf{0} & \textbf{0} & \textbf{0.0} \\ \hline \textcolor[HTML]{FF0000}{master.pl} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{3} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{worker.pl} & \textcolor[HTML]{FF0000}{29} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{20} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \textcolor[HTML]{FF0000}{zmq.pl} & \textcolor[HTML]{FF0000}{16} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} & \textcolor[HTML]{FF0000}{4} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0} & \textcolor[HTML]{FF0000}{0.0} \\ \hline \end{longtable} \end{document}