total uncompressed bytes
24.1 MB
total files
2238
Fix
226 wasted files
total waste: 2.5 MB
- z3/examples/tptp/tptp5.tab.c : 165.7 KB
- z3/src/test/lp/lp.cpp : 140.3 KB
- z3/examples/python/tutorial/html/guide-examples.htm : 104.2 KB
- z3/examples/c/test_capi.c : 92.7 KB
- z3/examples/python/tutorial/html/advanced-examples.htm : 85.4 KB
- z3/examples/dotnet/Program.cs : 83.4 KB
- z3/examples/python/tutorial/html/fixpoint-examples.htm : 82.7 KB
- z3/examples/tptp/tptp5.cpp : 81.8 KB
- z3/examples/java/JavaExample.java : 81.7 KB
- z3/src/test/polynomial.cpp : 80.3 KB
- z3/doc/z3api.cfg.in : 79.2 KB
- z3/examples/python/tutorial/jupyter/guide.ipynb : 71.5 KB
- z3/examples/tptp/tptp5.lex.cpp : 68.2 KB
- z3/resources/icon.jpg : 45.7 KB
- z3/doc/z3code.dox : 44.1 KB
- z3/src/test/upolynomial.cpp : 43.2 KB
- z3/examples/c++/example.cpp : 41.0 KB
- z3/examples/python/tutorial/jupyter/advanced.ipynb : 34.0 KB
- z3/examples/python/tutorial/html/strategies-examples.htm : 31.0 KB
- z3/src/test/udoc_relation.cpp : 30.2 KB
- z3/src/test/lp/nla_solver_test.cpp : 29.1 KB
- z3/examples/python/mini_quip.py : 25.6 KB
- z3/src/test/no_overflow.cpp : 25.4 KB
- z3/src/test/nlsat.cpp : 25.2 KB
- z3/src/test/algebraic.cpp : 20.8 KB
- z3/examples/maxsat/maxsat.c : 20.4 KB
- z3/src/test/mpff.cpp : 19.4 KB
- z3/src/test/quant_elim.cpp : 19.3 KB
- z3/src/test/sorting_network.cpp : 19.2 KB
- z3/src/test/ext_numeral.cpp : 18.3 KB
- z3/src/test/qe_arith.cpp : 18.0 KB
- z3/src/test/mpz.cpp : 16.8 KB
- z3/src/test/hilbert_basis.cpp : 16.6 KB
- z3/examples/msf/SolverFoundation.Plugin.Z3/Z3TermSolver.cs : 16.2 KB
- z3/src/test/rational.cpp : 16.0 KB
- z3/src/test/doc.cpp : 15.1 KB
- z3/src/test/interval.cpp : 14.6 KB
- z3/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs : 14.4 KB
- z3/src/test/lp/smt_reader.h : 13.4 KB
- z3/examples/ml/ml_example.ml : 13.1 KB
- z3/doc/mk_api_doc.py : 12.6 KB
- z3/examples/python/tutorial/jupyter/strategies.ipynb : 12.6 KB
- z3/src/test/model_based_opt.cpp : 12.4 KB
- z3/examples/python/tutorial/html/examples/sudoku.png : 12.3 KB
- z3/src/test/dl_product_relation.cpp : 12.0 KB
- z3/examples/python/mini_ic3.py : 11.8 KB
- z3/src/test/dl_relation.cpp : 11.7 KB
- z3/src/test/fuzzing/expr_rand.cpp : 11.0 KB
- z3/src/test/quant_solve.cpp : 9.6 KB
- z3/src/test/dl_query.cpp : 9.6 KB
- z3/src/test/cnf_backbones.cpp : 9.3 KB
- z3/src/test/lp/gomory_test.h : 9.2 KB
- z3/src/test/parray.cpp : 9.2 KB
- z3/examples/msf/Z3MSFPlugin.sln : 9.0 KB
- z3/examples/python/data/horn6.smt2 : 8.8 KB
- z3/src/test/pdd.cpp : 8.7 KB
- z3/src/test/karr.cpp : 7.9 KB
- z3/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPSolver.cs : 7.8 KB
- z3/src/test/simplifier.cpp : 7.8 KB
- z3/src/test/pb2bv.cpp : 7.7 KB
- z3/src/test/pdd_solver.cpp : 7.7 KB
- z3/src/test/main.cpp : 7.6 KB
- z3/examples/python/tutorial/html/examples/queens.png : 7.4 KB
- z3/examples/msf/Validator/Program.cs : 7.2 KB
- z3/src/math/lp/int_gcd_test.cpp : 7.0 KB
- z3/src/test/old_interval.cpp : 7.0 KB
- z3/src/test/bits.cpp : 6.8 KB
- z3/examples/python/mus/marco.py : 6.7 KB
- z3/src/test/bit_vector.cpp : 6.7 KB
- z3/src/test/polynorm.cpp : 6.6 KB
- z3/examples/msf/SolverFoundation.Plugin.Z3/SolverFoundation.Plugin.Z3.csproj : 6.3 KB
- z3/src/test/finder.cpp : 6.3 KB
- z3/src/test/ddnf.cpp : 6.3 KB
- z3/examples/msf/Validator/Validator.csproj : 5.4 KB
- z3/src/test/trigo.cpp : 5.4 KB
- z3/src/test/inf_rational.cpp : 5.3 KB
- z3/examples/python/mus/mss.py : 5.3 KB
- z3/src/test/rcf.cpp : 5.1 KB
- z3/examples/python/rc2.py : 4.9 KB
- z3/src/test/lp/argument_parser.h : 4.7 KB
- z3/src/test/theory_pb.cpp : 4.6 KB
- z3/examples/CMakeLists.txt : 4.5 KB
- z3/src/test/ast.cpp : 4.5 KB
- z3/src/test/diff_logic.cpp : 4.3 KB
- z3/src/test/get_implied_equalities.cpp : 4.3 KB
- z3/examples/msf/SolverFoundation.Plugin.Z3.Tests/SolverTests.cs : 4.3 KB
- z3/src/test/chashtable.cpp : 4.1 KB
- z3/src/test/simplex.cpp : 4.1 KB
- z3/src/test/smt2print_parse.cpp : 4.0 KB
- z3/doc/design_recfuns.md : 4.0 KB
- z3/src/test/heap.cpp : 4.0 KB
- z3/src/test/uint_set.cpp : 3.9 KB
- z3/examples/tptp/tptp5.tab.h : 3.9 KB
- z3/src/test/total_order.cpp : 3.8 KB
- z3/examples/msf/SolverFoundation.Plugin.Z3/Utils.cs : 3.8 KB
- z3/src/test/get_consequences.cpp : 3.6 KB
- z3/examples/python/complex/complex.py : 3.6 KB
- z3/examples/msf/Validator/App.config : 3.6 KB
- z3/examples/msf/SolverFoundation.Plugin.Z3.Tests/App.config : 3.6 KB
- z3/examples/msf/SolverFoundation.Plugin.Z3/App.config : 3.6 KB
- z3/src/test/sat_local_search.cpp : 3.6 KB
- z3/src/test/mpq.cpp : 3.5 KB
- z3/src/test/api.cpp : 3.5 KB
- z3/src/test/matcher.cpp : 3.4 KB
- z3/examples/python/trafficjam.py : 3.4 KB
- z3/examples/msf/Validator/MicrosoftSolverFoundationForExcel.dll.config : 3.4 KB
- z3/src/test/bit_blaster.cpp : 3.3 KB
- z3/src/test/object_allocator.cpp : 3.3 KB
- z3/examples/msf/SolverFoundation.Plugin.Z3.Tests/SolverFoundation.Plugin.Z3.Tests.csproj : 3.2 KB
- z3/src/test/CMakeLists.txt : 3.2 KB
- z3/src/test/dl_context.cpp : 3.1 KB
- z3/src/test/expr_rand.cpp : 3.1 KB
- z3/doc/CMakeLists.txt : 3.0 KB
- z3/examples/python/hamiltonian/hamiltonian.py : 2.9 KB
- z3/src/test/hashtable.cpp : 2.9 KB
- z3/src/test/var_subst.cpp : 2.9 KB
- z3/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseParams.cs : 2.9 KB
- z3/examples/msf/SolverFoundation.Plugin.Z3/AbortWorker.cs : 2.8 KB
- z3/src/test/dl_table.cpp : 2.8 KB
- z3/examples/python/data/horn4.smt2 : 2.7 KB
- z3/src/test/sat_user_scope.cpp : 2.7 KB
- z3/examples/msf/SolverFoundation.Plugin.Z3.Tests/ServiceTests.cs : 2.7 KB
- z3/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseDirective.cs : 2.5 KB
- z3/src/test/bdd.cpp : 2.5 KB
- z3/contrib/ci/scripts/test_z3_system_tests.sh : 2.4 KB
- z3/examples/python/all_interval_series.py : 2.4 KB
- z3/src/test/fixed_bit_vector.cpp : 2.4 KB
- z3/src/test/model_evaluator.cpp : 2.3 KB
- z3/src/test/permutation.cpp : 2.3 KB
- z3/src/test/im_float_config.h : 2.3 KB
- z3/src/test/hwf.cpp : 2.1 KB
- z3/src/test/horn_subsume_model_converter.cpp : 2.1 KB
- z3/src/test/fuzzing/expr_delta.cpp : 2.1 KB
- z3/src/test/tbv.cpp : 2.1 KB
- z3/src/test/cube_clause.cpp : 2.1 KB
- z3/src/test/model_retrieval.cpp : 2.0 KB
- z3/examples/c/CMakeLists.txt : 2.0 KB
- z3/examples/maxsat/CMakeLists.txt : 2.0 KB
- z3/src/test/test_util.h : 1.9 KB
- z3/src/test/mpf.cpp : 1.8 KB
- tests/lib.rs : 1.8 KB
- z3/src/test/lp/test_file_reader.h : 1.8 KB
- z3/src/test/simple_parser.cpp : 1.8 KB
- z3/src/test/datalog_parser.cpp : 1.7 KB
- z3/examples/c++/CMakeLists.txt : 1.6 KB
- z3/src/test/stack.cpp : 1.6 KB
- z3/examples/tptp/CMakeLists.txt : 1.6 KB
- z3/src/test/mpfx.cpp : 1.6 KB
- z3/src/test/expr_substitution.cpp : 1.6 KB
- z3/src/test/arith_rewriter.cpp : 1.6 KB
- z3/examples/python/data/horn1.smt2 : 1.6 KB
- z3/src/test/for_each_file.cpp : 1.6 KB
- z3/src/test/substitution.cpp : 1.6 KB
- z3/src/test/f2n.cpp : 1.6 KB
- z3/src/test/small_object_allocator.cpp : 1.5 KB
- z3/src/test/nlarith_util.cpp : 1.5 KB
- z3/src/test/model2expr.cpp : 1.5 KB
- z3/src/test/arith_simplifier_plugin.cpp : 1.5 KB
- z3/src/test/heap_trie.cpp : 1.5 KB
- z3/examples/msf/SolverFoundation.Plugin.Z3/Properties/AssemblyInfo.cs : 1.4 KB
- z3/examples/msf/SolverFoundation.Plugin.Z3.Tests/Properties/AssemblyInfo.cs : 1.4 KB
- z3/src/test/check_assumptions.cpp : 1.4 KB
- z3/examples/python/data/horn2.smt2 : 1.4 KB
- z3/examples/msf/Validator/Properties/AssemblyInfo.cs : 1.4 KB
- z3/src/test/api_bug.cpp : 1.4 KB
- z3/src/test/sat_lookahead.cpp : 1.4 KB
- z3/src/math/lp/int_gcd_test.h : 1.4 KB
- z3/src/test/vector.cpp : 1.3 KB
- z3/src/test/optional.cpp : 1.3 KB
- z3/examples/dotnet/CMakeLists.txt : 1.3 KB
- z3/src/test/dl_util.cpp : 1.3 KB
- z3/src/test/solver_pool.cpp : 1.3 KB
- z3/src/test/symbol.cpp : 1.2 KB
- z3/src/test/memory.cpp : 1.2 KB
- z3/src/test/list.cpp : 1.2 KB
- z3/src/test/fuzzing/expr_rand.h : 1.1 KB
- z3/examples/tptp/tptp5.h : 1.1 KB
- z3/examples/python/CMakeLists.txt : 1.1 KB
- z3/src/test/map.cpp : 1.1 KB
- z3/src/test/ex.cpp : 1.1 KB
- z3/examples/msf/README : 1.0 KB
- z3/examples/python/example.py : 1.0 KB
- z3/src/test/escaped.cpp : 1.0 KB
- z3/src/test/mpbq.cpp : 991 B
- z3/src/test/theory_dl.cpp : 971 B
- z3/src/test/symbol_table.cpp : 950 B
- z3/src/test/fuzzing/expr_delta.h : 937 B
- z3/src/test/proof_checker.cpp : 900 B
- z3/src/test/buffer.cpp : 886 B
- z3/src/test/string_buffer.cpp : 874 B
- z3/examples/python/parallel.py : 849 B
- z3/src/test/prime_generator.cpp : 818 B
- z3/examples/ml/README : 797 B
- z3/examples/python/socrates.py : 793 B
- z3/src/test/smt_context.cpp : 752 B
- z3/src/test/factor_rewriter.cpp : 655 B
- z3/src/test/lp/CMakeLists.txt : 654 B
- z3/examples/tptp/README : 628 B
- z3/examples/python/visitor.py : 621 B
- z3/doc/README : 593 B
- z3/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPParams.cs : 583 B
- z3/examples/python/data/horn5.smt2 : 573 B
- z3/examples/java/README : 546 B
- z3/src/test/for_each_file.h : 545 B
- z3/examples/python/union_sort.py : 543 B
- z3/doc/website.dox.in : 543 B
- z3/examples/maxsat/README : 515 B
- z3/examples/msf/SolverFoundation.Plugin.Z3/Z3TermParams.cs : 510 B
- z3/contrib/cmake/src/test/lp/CMakeLists.txt : 496 B
- z3/src/test/random.cpp : 431 B
- z3/examples/python/data/horn3.smt2 : 423 B
- z3/examples/c++/README : 417 B
- z3/examples/c/README : 414 B
- scripts/generate_enums.sh : 373 B
- z3/src/test/region.cpp : 322 B
- z3/src/test/lp/lp_main.cpp : 313 B
- z3/examples/dotnet/dotnet.csproj : 274 B
- z3/examples/python/tutorial/jupyter/README.md : 252 B
- z3/examples/maxsat/ex.smt : 247 B
- z3/examples/msf/SolverFoundation.Plugin.Z3/Z3TermDirective.cs : 229 B
- z3/examples/msf/SolverFoundation.Plugin.Z3/Z3MILPDirective.cs : 229 B
- z3/src/test/timeout.cpp : 206 B
- z3/src/test/fuzzing/CMakeLists.txt : 169 B
- z3/examples/python/README : 156 B
- z3/examples/dotnet/README : 146 B
- z3/examples/python/tutorial/html/index.html : 81 B