API tools faq
paste
Advertisement
Guest User

SBV and Z3

a guest
Jul 1st, 2013
175
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 50.29 KB | None | 0 0
raw download clone embed print report
  1. Mukeshs-MacBook-Pro:SMT mukeshtiwari$ git clone https://git01.codeplex.com/z3 -b unstable
  2. Cloning into 'z3'...
  3. remote: Counting objects: 16070, done.
  4. remote: Compressing objects: 100% (3928/3928), done.
  5. remote: Total 16070 (delta 12057), reused 16070 (delta 12057)
  6. Receiving objects: 100% (16070/16070), 7.62 MiB | 287 KiB/s, done.
  7. Resolving deltas: 100% (12057/12057), done.
  8. Mukeshs-MacBook-Pro:SMT mukeshtiwari$ ls
  9. z3
  10. Mukeshs-MacBook-Pro:SMT mukeshtiwari$ cd z3/
  11. Mukeshs-MacBook-Pro:z3 mukeshtiwari$ ls
  12. LICENSE.txt README RELEASE_NOTES configure doc examples scripts src
  13. Mukeshs-MacBook-Pro:z3 mukeshtiwari$ python
  14. python python2.5 python2.6 python2.7 pythonw pythonw2.6
  15. python-config python2.5-config python2.6-config python2.7-config pythonw2.5 pythonw2.7
  16. Mukeshs-MacBook-Pro:z3 mukeshtiwari$ python s
  17. scripts/ src/
  18. Mukeshs-MacBook-Pro:z3 mukeshtiwari$ python scripts/mk_make.py
  19. New component: 'util'
  20. New component: 'polynomial'
  21. New component: 'sat'
  22. New component: 'nlsat'
  23. New component: 'interval'
  24. New component: 'realclosure'
  25. New component: 'subpaving'
  26. New component: 'ast'
  27. New component: 'rewriter'
  28. New component: 'normal_forms'
  29. New component: 'model'
  30. New component: 'tactic'
  31. New component: 'substitution'
  32. New component: 'parser_util'
  33. New component: 'grobner'
  34. New component: 'euclid'
  35. New component: 'core_tactics'
  36. New component: 'sat_tactic'
  37. New component: 'arith_tactics'
  38. New component: 'nlsat_tactic'
  39. New component: 'subpaving_tactic'
  40. New component: 'aig_tactic'
  41. New component: 'solver'
  42. New component: 'cmd_context'
  43. New component: 'extra_cmds'
  44. New component: 'smt2parser'
  45. New component: 'proof_checker'
  46. New component: 'simplifier'
  47. New component: 'macros'
  48. New component: 'pattern'
  49. New component: 'bit_blaster'
  50. New component: 'smt_params'
  51. New component: 'proto_model'
  52. New component: 'smt'
  53. New component: 'user_plugin'
  54. New component: 'bv_tactics'
  55. New component: 'fuzzing'
  56. New component: 'fpa'
  57. New component: 'smt_tactic'
  58. New component: 'sls_tactic'
  59. New component: 'muz_qe'
  60. New component: 'smtlogic_tactics'
  61. New component: 'ufbv_tactic'
  62. New component: 'portfolio'
  63. New component: 'smtparser'
  64. New component: 'api'
  65. New component: 'shell'
  66. New component: 'test'
  67. New component: 'api_dll'
  68. New component: 'dotnet'
  69. New component: 'java'
  70. New component: 'cpp'
  71. Python bindinds directory was detected.
  72. New component: 'cpp_example'
  73. New component: 'c_example'
  74. New component: 'maxsat'
  75. New component: 'dotnet_example'
  76. New component: 'java_example'
  77. New component: 'py_example'
  78. Generated 'src/util/version.h'
  79. Updated 'src/api/dotnet/Properties/AssemblyInfo'
  80. Generated 'src/ast/pp_params.hpp'
  81. Generated 'src/ast/normal_forms/nnf_params.hpp'
  82. Generated 'src/ast/pattern/pattern_inference_params_helper.hpp'
  83. Generated 'src/ast/rewriter/arith_rewriter_params.hpp'
  84. Generated 'src/ast/rewriter/array_rewriter_params.hpp'
  85. Generated 'src/ast/rewriter/bool_rewriter_params.hpp'
  86. Generated 'src/ast/rewriter/bv_rewriter_params.hpp'
  87. Generated 'src/ast/rewriter/poly_rewriter_params.hpp'
  88. Generated 'src/ast/rewriter/rewriter_params.hpp'
  89. Generated 'src/ast/simplifier/arith_simplifier_params_helper.hpp'
  90. Generated 'src/ast/simplifier/array_simplifier_params_helper.hpp'
  91. Generated 'src/ast/simplifier/bv_simplifier_params_helper.hpp'
  92. Generated 'src/math/polynomial/algebraic_params.hpp'
  93. Generated 'src/math/realclosure/rcf_params.hpp'
  94. Generated 'src/model/model_evaluator_params.hpp'
  95. Generated 'src/model/model_params.hpp'
  96. Generated 'src/muz_qe/fixedpoint_params.hpp'
  97. Generated 'src/nlsat/nlsat_params.hpp'
  98. Generated 'src/parsers/util/parser_params.hpp'
  99. Generated 'src/sat/sat_asymm_branch_params.hpp'
  100. Generated 'src/sat/sat_params.hpp'
  101. Generated 'src/sat/sat_scc_params.hpp'
  102. Generated 'src/sat/sat_simplifier_params.hpp'
  103. Generated 'src/smt/params/smt_params_helper.hpp'
  104. Generated 'src/solver/combined_solver_params.hpp'
  105. Generated 'src/ast/pattern/database.h'
  106. Generated 'src/shell/install_tactic.cpp'
  107. Generated 'src/test/install_tactic.cpp'
  108. Generated 'src/api/dll/install_tactic.cpp'
  109. Generated 'src/shell/mem_initializer.cpp'
  110. Generated 'src/test/mem_initializer.cpp'
  111. Generated 'src/api/dll/mem_initializer.cpp'
  112. Generated 'src/shell/gparams_register_modules.cpp'
  113. Generated 'src/test/gparams_register_modules.cpp'
  114. Generated 'src/api/dll/gparams_register_modules.cpp'
  115. Generated 'src/api/python/z3consts.py'
  116. Generated 'src/api/dotnet/Enumerations.cs'
  117. Generated 'src/api/api_log_macros.h'
  118. Generated 'src/api/api_log_macros.cpp'
  119. Generated 'src/api/api_commands.cpp'
  120. Generated 'src/api/python/z3core.py'
  121. Generated 'src/api/dotnet/Native.cs'
  122. Listing src/api/python ...
  123. Compiling src/api/python/z3.py ...
  124. Compiling src/api/python/z3consts.py ...
  125. Compiling src/api/python/z3core.py ...
  126. Compiling src/api/python/z3num.py ...
  127. Compiling src/api/python/z3poly.py ...
  128. Compiling src/api/python/z3printer.py ...
  129. Compiling src/api/python/z3rcf.py ...
  130. Compiling src/api/python/z3test.py ...
  131. Compiling src/api/python/z3types.py ...
  132. Copied 'z3.py'
  133. Copied 'z3consts.py'
  134. Copied 'z3core.py'
  135. Copied 'z3num.py'
  136. Copied 'z3poly.py'
  137. Copied 'z3printer.py'
  138. Copied 'z3rcf.py'
  139. Copied 'z3test.py'
  140. Copied 'z3types.py'
  141. Generated 'z3.pyc'
  142. Generated 'z3consts.pyc'
  143. Generated 'z3core.pyc'
  144. Generated 'z3num.pyc'
  145. Generated 'z3poly.pyc'
  146. Generated 'z3printer.pyc'
  147. Generated 'z3rcf.pyc'
  148. Generated 'z3test.pyc'
  149. Generated 'z3types.pyc'
  150. Testing ar...
  151. Testing g++...
  152. Testing gcc...
  153. Testing OpenMP...
  154. Host platform: Darwin
  155. C++ Compiler: g++
  156. C Compiler : gcc
  157. Arithmetic: internal
  158. OpenMP: True
  159. Prefix: /Library
  160. 64-bit: True
  161. Python version: 2.7
  162. Writing build/Makefile
  163. Copied Z3Py example 'example.py' to 'build'
  164. Makefile was successfully generated.
  165. python packages dir: /Library/Python/2.7/site-packages
  166. compilation mode: Release
  167. Type 'cd build; make' to build Z3
  168. Mukeshs-MacBook-Pro:z3 mukeshtiwari$ cd build/
  169. Mukeshs-MacBook-Pro:build mukeshtiwari$ make
  170. src/shell/datalog_frontend.cpp
  171. src/shell/dimacs_frontend.cpp
  172. src/shell/gparams_register_modules.cpp
  173. src/shell/install_tactic.cpp
  174. src/shell/main.cpp
  175. src/shell/mem_initializer.cpp
  176. src/shell/smtlib_frontend.cpp
  177. src/shell/z3_log_frontend.cpp
  178. src/api/api_algebraic.cpp
  179. src/api/api_arith.cpp
  180. src/api/api_array.cpp
  181. src/api/api_ast.cpp
  182. src/api/api_ast_map.cpp
  183. src/api/api_ast_vector.cpp
  184. src/api/api_bv.cpp
  185. src/api/api_commands.cpp
  186. src/api/api_config_params.cpp
  187. src/api/api_context.cpp
  188. src/api/api_datalog.cpp
  189. src/api/api_datatype.cpp
  190. src/api/api_goal.cpp
  191. src/api/api_log.cpp
  192. src/api/api_log_macros.cpp
  193. src/api/api_model.cpp
  194. src/api/api_numeral.cpp
  195. src/api/api_params.cpp
  196. src/api/api_parsers.cpp
  197. src/api/api_polynomial.cpp
  198. src/api/api_quant.cpp
  199. src/api/api_rcf.cpp
  200. src/api/api_solver.cpp
  201. src/api/api_solver_old.cpp
  202. src/api/api_stats.cpp
  203. src/api/api_tactic.cpp
  204. src/api/api_user_theory.cpp
  205. src/api/z3_replayer.cpp
  206. src/parsers/smt/smtlib.cpp
  207. src/parsers/smt/smtlib_solver.cpp
  208. src/parsers/smt/smtparser.cpp
  209. src/tactic/portfolio/default_tactic.cpp
  210. src/tactic/portfolio/smt_strategic_solver.cpp
  211. src/tactic/ufbv/macro_finder_tactic.cpp
  212. src/tactic/ufbv/quasi_macros_tactic.cpp
  213. src/tactic/ufbv/ufbv_rewriter.cpp
  214. src/tactic/ufbv/ufbv_rewriter_tactic.cpp
  215. src/tactic/ufbv/ufbv_tactic.cpp
  216. src/tactic/smtlogics/nra_tactic.cpp
  217. src/tactic/smtlogics/qfaufbv_tactic.cpp
  218. src/tactic/smtlogics/qfauflia_tactic.cpp
  219. src/tactic/smtlogics/qfbv_tactic.cpp
  220. src/tactic/smtlogics/qfidl_tactic.cpp
  221. src/tactic/smtlogics/qflia_tactic.cpp
  222. src/tactic/smtlogics/qflra_tactic.cpp
  223. src/tactic/smtlogics/qfnia_tactic.cpp
  224. src/tactic/smtlogics/qfnra_tactic.cpp
  225. src/tactic/smtlogics/qfuf_tactic.cpp
  226. src/tactic/smtlogics/qfufbv_tactic.cpp
  227. src/tactic/smtlogics/quant_tactics.cpp
  228. src/muz_qe/aig_exporter.cpp
  229. src/muz_qe/arith_bounds_tactic.cpp
  230. src/muz_qe/clp_context.cpp
  231. src/muz_qe/datalog_parser.cpp
  232. src/muz_qe/dl_base.cpp
  233. src/muz_qe/dl_bmc_engine.cpp
  234. src/muz_qe/dl_boogie_proof.cpp
  235. src/muz_qe/dl_bound_relation.cpp
  236. src/muz_qe/dl_check_table.cpp
  237. src/muz_qe/dl_cmds.cpp
  238. src/muz_qe/dl_compiler.cpp
  239. src/muz_qe/dl_context.cpp
  240. src/muz_qe/dl_costs.cpp
  241. src/muz_qe/dl_external_relation.cpp
  242. src/muz_qe/dl_finite_product_relation.cpp
  243. src/muz_qe/dl_instruction.cpp
  244. src/muz_qe/dl_interval_relation.cpp
  245. src/muz_qe/dl_mk_array_blast.cpp
  246. src/muz_qe/dl_mk_backwards.cpp
  247. src/muz_qe/dl_mk_bit_blast.cpp
  248. src/muz_qe/dl_mk_coalesce.cpp
  249. src/muz_qe/dl_mk_coi_filter.cpp
  250. src/muz_qe/dl_mk_explanations.cpp
  251. src/muz_qe/dl_mk_filter_rules.cpp
  252. src/muz_qe/dl_mk_interp_tail_simplifier.cpp
  253. src/muz_qe/dl_mk_karr_invariants.cpp
  254. src/muz_qe/dl_mk_loop_counter.cpp
  255. src/muz_qe/dl_mk_magic_sets.cpp
  256. src/muz_qe/dl_mk_magic_symbolic.cpp
  257. src/muz_qe/dl_mk_partial_equiv.cpp
  258. src/muz_qe/dl_mk_quantifier_abstraction.cpp
  259. src/muz_qe/dl_mk_quantifier_instantiation.cpp
  260. src/muz_qe/dl_mk_rule_inliner.cpp
  261. src/muz_qe/dl_mk_similarity_compressor.cpp
  262. src/muz_qe/dl_mk_simple_joins.cpp
  263. src/muz_qe/dl_mk_slice.cpp
  264. src/muz_qe/dl_mk_subsumption_checker.cpp
  265. src/muz_qe/dl_mk_unbound_compressor.cpp
  266. src/muz_qe/dl_mk_unfold.cpp
  267. src/muz_qe/dl_product_relation.cpp
  268. src/muz_qe/dl_relation_manager.cpp
  269. src/muz_qe/dl_rule.cpp
  270. src/muz_qe/dl_rule_set.cpp
  271. src/muz_qe/dl_rule_subsumption_index.cpp
  272. src/muz_qe/dl_rule_transformer.cpp
  273. src/muz_qe/dl_sieve_relation.cpp
  274. src/muz_qe/dl_sparse_table.cpp
  275. src/muz_qe/dl_table.cpp
  276. src/muz_qe/dl_table_relation.cpp
  277. src/muz_qe/dl_util.cpp
  278. src/muz_qe/equiv_proof_converter.cpp
  279. src/muz_qe/hilbert_basis.cpp
  280. src/muz_qe/hnf.cpp
  281. src/muz_qe/horn_subsume_model_converter.cpp
  282. src/muz_qe/horn_tactic.cpp
  283. src/muz_qe/model2expr.cpp
  284. src/muz_qe/nlarith_util.cpp
  285. src/muz_qe/pdr_context.cpp
  286. src/muz_qe/pdr_dl_interface.cpp
  287. src/muz_qe/pdr_farkas_learner.cpp
  288. src/muz_qe/pdr_generalizers.cpp
  289. src/muz_qe/pdr_manager.cpp
  290. src/muz_qe/pdr_prop_solver.cpp
  291. src/muz_qe/pdr_reachable_cache.cpp
  292. src/muz_qe/pdr_smt_context_manager.cpp
  293. src/muz_qe/pdr_sym_mux.cpp
  294. src/muz_qe/pdr_util.cpp
  295. src/muz_qe/proof_utils.cpp
  296. src/muz_qe/qe.cpp
  297. src/muz_qe/qe_arith_plugin.cpp
  298. src/muz_qe/qe_array_plugin.cpp
  299. src/muz_qe/qe_bool_plugin.cpp
  300. src/muz_qe/qe_bv_plugin.cpp
  301. src/muz_qe/qe_cmd.cpp
  302. src/muz_qe/qe_datatype_plugin.cpp
  303. src/muz_qe/qe_dl_plugin.cpp
  304. src/muz_qe/qe_lite.cpp
  305. src/muz_qe/qe_sat_tactic.cpp
  306. src/muz_qe/qe_tactic.cpp
  307. src/muz_qe/rel_context.cpp
  308. src/muz_qe/replace_proof_converter.cpp
  309. src/muz_qe/tab_context.cpp
  310. src/muz_qe/unit_subsumption_tactic.cpp
  311. src/muz_qe/vsubst_tactic.cpp
  312. src/tactic/sls/sls_tactic.cpp
  313. src/smt/tactic/ctx_solver_simplify_tactic.cpp
  314. src/smt/tactic/smt_tactic.cpp
  315. src/tactic/fpa/fpa2bv_converter.cpp
  316. src/tactic/fpa/fpa2bv_tactic.cpp
  317. src/tactic/fpa/qffpa_tactic.cpp
  318. src/tactic/bv/bit_blaster_model_converter.cpp
  319. src/tactic/bv/bit_blaster_tactic.cpp
  320. src/tactic/bv/bv1_blaster_tactic.cpp
  321. src/tactic/bv/bv_size_reduction_tactic.cpp
  322. src/tactic/bv/max_bv_sharing_tactic.cpp
  323. src/smt/user_plugin/user_decl_plugin.cpp
  324. src/smt/user_plugin/user_simplifier_plugin.cpp
  325. src/smt/user_plugin/user_smt_theory.cpp
  326. src/smt/arith_eq_adapter.cpp
  327. src/smt/arith_eq_solver.cpp
  328. src/smt/asserted_formulas.cpp
  329. src/smt/cached_var_subst.cpp
  330. src/smt/cost_evaluator.cpp
  331. src/smt/dyn_ack.cpp
  332. src/smt/elim_term_ite.cpp
  333. src/smt/expr_context_simplifier.cpp
  334. src/smt/fingerprints.cpp
  335. src/smt/mam.cpp
  336. src/smt/old_interval.cpp
  337. src/smt/qi_queue.cpp
  338. src/smt/smt_almost_cg_table.cpp
  339. src/smt/smt_case_split_queue.cpp
  340. src/smt/smt_cg_table.cpp
  341. src/smt/smt_checker.cpp
  342. src/smt/smt_clause.cpp
  343. src/smt/smt_conflict_resolution.cpp
  344. src/smt/smt_context.cpp
  345. src/smt/smt_context_inv.cpp
  346. src/smt/smt_context_pp.cpp
  347. src/smt/smt_context_stat.cpp
  348. src/smt/smt_enode.cpp
  349. src/smt/smt_for_each_relevant_expr.cpp
  350. src/smt/smt_implied_equalities.cpp
  351. src/smt/smt_internalizer.cpp
  352. src/smt/smt_justification.cpp
  353. src/smt/smt_kernel.cpp
  354. src/smt/smt_literal.cpp
  355. src/smt/smt_model_checker.cpp
  356. src/smt/smt_model_finder.cpp
  357. src/smt/smt_model_generator.cpp
  358. src/smt/smt_quantifier.cpp
  359. src/smt/smt_quantifier_stat.cpp
  360. src/smt/smt_quick_checker.cpp
  361. src/smt/smt_relevancy.cpp
  362. src/smt/smt_setup.cpp
  363. src/smt/smt_solver.cpp
  364. src/smt/smt_statistics.cpp
  365. src/smt/smt_theory.cpp
  366. src/smt/smt_value_sort.cpp
  367. src/smt/theory_arith.cpp
  368. src/smt/theory_array.cpp
  369. src/smt/theory_array_base.cpp
  370. src/smt/theory_array_full.cpp
  371. src/smt/theory_bv.cpp
  372. src/smt/theory_datatype.cpp
  373. src/smt/theory_dense_diff_logic.cpp
  374. src/smt/theory_diff_logic.cpp
  375. src/smt/theory_dl.cpp
  376. src/smt/theory_dummy.cpp
  377. src/smt/theory_horn_ineq.cpp
  378. src/smt/theory_utvpi.cpp
  379. src/smt/uses_theory.cpp
  380. src/smt/watch_list.cpp
  381. src/smt/proto_model/array_factory.cpp
  382. src/smt/proto_model/datatype_factory.cpp
  383. src/smt/proto_model/numeral_factory.cpp
  384. src/smt/proto_model/proto_model.cpp
  385. src/smt/proto_model/struct_factory.cpp
  386. src/smt/proto_model/value_factory.cpp
  387. src/smt/params/dyn_ack_params.cpp
  388. src/smt/params/preprocessor_params.cpp
  389. src/smt/params/qi_params.cpp
  390. src/smt/params/smt_params.cpp
  391. src/smt/params/theory_arith_params.cpp
  392. src/smt/params/theory_bv_params.cpp
  393. /usr/bin/ranlib: file: smt/params/smt_params.a(dyn_ack_params.o) has no symbols
  394. src/ast/rewriter/bit_blaster/bit_blaster.cpp
  395. src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
  396. src/ast/pattern/expr_pattern_match.cpp
  397. src/ast/pattern/pattern_inference.cpp
  398. src/ast/pattern/pattern_inference_params.cpp
  399. src/ast/macros/macro_finder.cpp
  400. src/ast/macros/macro_manager.cpp
  401. src/ast/macros/macro_util.cpp
  402. src/ast/macros/quasi_macros.cpp
  403. src/ast/simplifier/arith_simplifier_params.cpp
  404. src/ast/simplifier/arith_simplifier_plugin.cpp
  405. src/ast/simplifier/array_simplifier_params.cpp
  406. src/ast/simplifier/array_simplifier_plugin.cpp
  407. src/ast/simplifier/basic_simplifier_plugin.cpp
  408. src/ast/simplifier/bit2int.cpp
  409. src/ast/simplifier/bv_elim.cpp
  410. src/ast/simplifier/bv_simplifier_params.cpp
  411. src/ast/simplifier/bv_simplifier_plugin.cpp
  412. src/ast/simplifier/datatype_simplifier_plugin.cpp
  413. src/ast/simplifier/distribute_forall.cpp
  414. src/ast/simplifier/elim_bounds.cpp
  415. src/ast/simplifier/inj_axiom.cpp
  416. src/ast/simplifier/maximise_ac_sharing.cpp
  417. src/ast/simplifier/poly_simplifier_plugin.cpp
  418. src/ast/simplifier/pull_ite_tree.cpp
  419. src/ast/simplifier/push_app_ite.cpp
  420. src/ast/simplifier/simplifier.cpp
  421. src/ast/simplifier/simplifier_plugin.cpp
  422. src/ast/proof_checker/proof_checker.cpp
  423. src/parsers/smt2/smt2parser.cpp
  424. src/parsers/smt2/smt2scanner.cpp
  425. src/cmd_context/extra_cmds/dbg_cmds.cpp
  426. src/cmd_context/extra_cmds/polynomial_cmds.cpp
  427. src/cmd_context/extra_cmds/subpaving_cmds.cpp
  428. src/cmd_context/basic_cmds.cpp
  429. src/cmd_context/check_logic.cpp
  430. src/cmd_context/cmd_context.cpp
  431. src/cmd_context/cmd_context_to_goal.cpp
  432. src/cmd_context/cmd_util.cpp
  433. src/cmd_context/context_params.cpp
  434. src/cmd_context/echo_tactic.cpp
  435. src/cmd_context/eval_cmd.cpp
  436. src/cmd_context/parametric_cmd.cpp
  437. src/cmd_context/pdecl.cpp
  438. src/cmd_context/simplify_cmd.cpp
  439. src/cmd_context/tactic_cmds.cpp
  440. src/cmd_context/tactic_manager.cpp
  441. src/solver/check_sat_result.cpp
  442. src/solver/combined_solver.cpp
  443. src/solver/solver.cpp
  444. src/solver/solver_na2as.cpp
  445. src/solver/tactic2solver.cpp
  446. src/tactic/aig/aig.cpp
  447. src/tactic/aig/aig_tactic.cpp
  448. src/math/subpaving/tactic/expr2subpaving.cpp
  449. src/math/subpaving/tactic/subpaving_tactic.cpp
  450. src/nlsat/tactic/goal2nlsat.cpp
  451. src/nlsat/tactic/nlsat_tactic.cpp
  452. src/nlsat/tactic/qfnra_nlsat_tactic.cpp
  453. src/tactic/arith/add_bounds_tactic.cpp
  454. src/tactic/arith/bound_manager.cpp
  455. src/tactic/arith/bound_propagator.cpp
  456. src/tactic/arith/bv2int_rewriter.cpp
  457. src/tactic/arith/bv2real_rewriter.cpp
  458. src/tactic/arith/degree_shift_tactic.cpp
  459. src/tactic/arith/diff_neq_tactic.cpp
  460. src/tactic/arith/factor_tactic.cpp
  461. src/tactic/arith/fix_dl_var_tactic.cpp
  462. src/tactic/arith/fm_tactic.cpp
  463. src/tactic/arith/lia2pb_tactic.cpp
  464. src/tactic/arith/linear_equation.cpp
  465. src/tactic/arith/nla2bv_tactic.cpp
  466. src/tactic/arith/normalize_bounds_tactic.cpp
  467. src/tactic/arith/pb2bv_model_converter.cpp
  468. src/tactic/arith/pb2bv_tactic.cpp
  469. src/tactic/arith/probe_arith.cpp
  470. src/tactic/arith/propagate_ineqs_tactic.cpp
  471. src/tactic/arith/purify_arith_tactic.cpp
  472. src/tactic/arith/recover_01_tactic.cpp
  473. src/sat/tactic/atom2bool_var.cpp
  474. src/sat/tactic/goal2sat.cpp
  475. src/sat/tactic/sat_tactic.cpp
  476. src/tactic/core/cofactor_elim_term_ite.cpp
  477. src/tactic/core/cofactor_term_ite_tactic.cpp
  478. src/tactic/core/ctx_simplify_tactic.cpp
  479. src/tactic/core/der_tactic.cpp
  480. src/tactic/core/distribute_forall_tactic.cpp
  481. src/tactic/core/elim_term_ite_tactic.cpp
  482. src/tactic/core/elim_uncnstr_tactic.cpp
  483. src/tactic/core/nnf_tactic.cpp
  484. src/tactic/core/occf_tactic.cpp
  485. src/tactic/core/propagate_values_tactic.cpp
  486. src/tactic/core/reduce_args_tactic.cpp
  487. src/tactic/core/simplify_tactic.cpp
  488. src/tactic/core/solve_eqs_tactic.cpp
  489. src/tactic/core/split_clause_tactic.cpp
  490. src/tactic/core/symmetry_reduce_tactic.cpp
  491. src/tactic/core/tseitin_cnf_tactic.cpp
  492. src/math/euclid/euclidean_solver.cpp
  493. src/math/grobner/grobner.cpp
  494. src/parsers/util/cost_parser.cpp
  495. src/parsers/util/pattern_validation.cpp
  496. src/parsers/util/scanner.cpp
  497. src/parsers/util/simple_parser.cpp
  498. src/ast/substitution/matcher.cpp
  499. src/ast/substitution/substitution.cpp
  500. src/ast/substitution/substitution_tree.cpp
  501. src/ast/substitution/unifier.cpp
  502. src/tactic/extension_model_converter.cpp
  503. src/tactic/filter_model_converter.cpp
  504. src/tactic/goal.cpp
  505. src/tactic/goal_num_occurs.cpp
  506. src/tactic/goal_shared_occs.cpp
  507. src/tactic/goal_util.cpp
  508. src/tactic/model_converter.cpp
  509. src/tactic/probe.cpp
  510. src/tactic/proof_converter.cpp
  511. src/tactic/tactic.cpp
  512. src/tactic/tactical.cpp
  513. src/model/func_interp.cpp
  514. src/model/model.cpp
  515. src/model/model_core.cpp
  516. src/model/model_evaluator.cpp
  517. src/model/model_pp.cpp
  518. src/model/model_smt2_pp.cpp
  519. src/model/model_v2_pp.cpp
  520. src/ast/normal_forms/defined_names.cpp
  521. src/ast/normal_forms/name_exprs.cpp
  522. src/ast/normal_forms/nnf.cpp
  523. src/ast/normal_forms/pull_quant.cpp
  524. src/ast/rewriter/arith_rewriter.cpp
  525. src/ast/rewriter/array_rewriter.cpp
  526. src/ast/rewriter/ast_counter.cpp
  527. src/ast/rewriter/bool_rewriter.cpp
  528. src/ast/rewriter/bv_rewriter.cpp
  529. src/ast/rewriter/datatype_rewriter.cpp
  530. src/ast/rewriter/der.cpp
  531. src/ast/rewriter/dl_rewriter.cpp
  532. src/ast/rewriter/expr_replacer.cpp
  533. src/ast/rewriter/expr_safe_replace.cpp
  534. src/ast/rewriter/factor_rewriter.cpp
  535. src/ast/rewriter/float_rewriter.cpp
  536. src/ast/rewriter/mk_simplified_app.cpp
  537. src/ast/rewriter/quant_hoist.cpp
  538. src/ast/rewriter/rewriter.cpp
  539. src/ast/rewriter/th_rewriter.cpp
  540. src/ast/rewriter/var_subst.cpp
  541. src/ast/act_cache.cpp
  542. src/ast/arith_decl_plugin.cpp
  543. src/ast/array_decl_plugin.cpp
  544. src/ast/ast.cpp
  545. src/ast/ast_ll_pp.cpp
  546. src/ast/ast_lt.cpp
  547. src/ast/ast_printer.cpp
  548. src/ast/ast_smt2_pp.cpp
  549. src/ast/ast_smt_pp.cpp
  550. src/ast/ast_translation.cpp
  551. src/ast/ast_util.cpp
  552. src/ast/bv_decl_plugin.cpp
  553. src/ast/datatype_decl_plugin.cpp
  554. src/ast/decl_collector.cpp
  555. src/ast/dl_decl_plugin.cpp
  556. src/ast/expr2polynomial.cpp
  557. src/ast/expr2var.cpp
  558. src/ast/expr_abstract.cpp
  559. src/ast/expr_functors.cpp
  560. src/ast/expr_map.cpp
  561. src/ast/expr_stat.cpp
  562. src/ast/expr_substitution.cpp
  563. src/ast/float_decl_plugin.cpp
  564. src/ast/for_each_ast.cpp
  565. src/ast/for_each_expr.cpp
  566. src/ast/format.cpp
  567. src/ast/func_decl_dependencies.cpp
  568. src/ast/has_free_vars.cpp
  569. src/ast/macro_substitution.cpp
  570. src/ast/num_occurs.cpp
  571. src/ast/occurs.cpp
  572. src/ast/pp.cpp
  573. src/ast/reg_decl_plugins.cpp
  574. src/ast/seq_decl_plugin.cpp
  575. src/ast/shared_occs.cpp
  576. src/ast/static_features.cpp
  577. src/ast/used_vars.cpp
  578. src/ast/well_sorted.cpp
  579. src/math/subpaving/subpaving.cpp
  580. src/math/subpaving/subpaving_hwf.cpp
  581. src/math/subpaving/subpaving_mpf.cpp
  582. src/math/subpaving/subpaving_mpff.cpp
  583. src/math/subpaving/subpaving_mpfx.cpp
  584. src/math/subpaving/subpaving_mpq.cpp
  585. src/math/realclosure/mpz_matrix.cpp
  586. src/math/realclosure/realclosure.cpp
  587. src/math/interval/interval_mpq.cpp
  588. src/nlsat/nlsat_clause.cpp
  589. src/nlsat/nlsat_evaluator.cpp
  590. src/nlsat/nlsat_explain.cpp
  591. src/nlsat/nlsat_interval_set.cpp
  592. src/nlsat/nlsat_solver.cpp
  593. src/nlsat/nlsat_types.cpp
  594. src/sat/dimacs.cpp
  595. src/sat/sat_asymm_branch.cpp
  596. src/sat/sat_clause.cpp
  597. src/sat/sat_clause_set.cpp
  598. src/sat/sat_clause_use_list.cpp
  599. src/sat/sat_cleaner.cpp
  600. src/sat/sat_config.cpp
  601. src/sat/sat_elim_eqs.cpp
  602. src/sat/sat_iff3_finder.cpp
  603. src/sat/sat_integrity_checker.cpp
  604. src/sat/sat_model_converter.cpp
  605. src/sat/sat_probing.cpp
  606. src/sat/sat_scc.cpp
  607. src/sat/sat_simplifier.cpp
  608. src/sat/sat_solver.cpp
  609. src/sat/sat_watched.cpp
  610. src/math/polynomial/algebraic_numbers.cpp
  611. src/math/polynomial/polynomial.cpp
  612. src/math/polynomial/polynomial_cache.cpp
  613. src/math/polynomial/polynomial_factorization.cpp
  614. src/math/polynomial/rpolynomial.cpp
  615. src/math/polynomial/sexpr2upolynomial.cpp
  616. src/math/polynomial/upolynomial.cpp
  617. src/math/polynomial/upolynomial_factorization.cpp
  618. /usr/bin/ranlib: file: math/polynomial/polynomial.a(polynomial_factorization.o) has no symbols
  619. src/util/approx_nat.cpp
  620. src/util/approx_set.cpp
  621. src/util/bit_util.cpp
  622. src/util/bit_vector.cpp
  623. src/util/cmd_context_types.cpp
  624. src/util/common_msgs.cpp
  625. src/util/cooperate.cpp
  626. src/util/debug.cpp
  627. src/util/env_params.cpp
  628. src/util/gparams.cpp
  629. src/util/hash.cpp
  630. src/util/hwf.cpp
  631. src/util/inf_int_rational.cpp
  632. src/util/inf_rational.cpp
  633. src/util/inf_s_integer.cpp
  634. src/util/lbool.cpp
  635. src/util/luby.cpp
  636. src/util/memory_manager.cpp
  637. src/util/mpbq.cpp
  638. src/util/mpf.cpp
  639. src/util/mpff.cpp
  640. src/util/mpfx.cpp
  641. src/util/mpn.cpp
  642. src/util/mpq.cpp
  643. src/util/mpq_inf.cpp
  644. src/util/mpz.cpp
  645. src/util/page.cpp
  646. src/util/params.cpp
  647. src/util/permutation.cpp
  648. src/util/prime_generator.cpp
  649. src/util/rational.cpp
  650. src/util/region.cpp
  651. src/util/s_integer.cpp
  652. src/util/scoped_ctrl_c.cpp
  653. src/util/scoped_timer.cpp
  654. src/util/sexpr.cpp
  655. src/util/small_object_allocator.cpp
  656. src/util/smt2_util.cpp
  657. src/util/stack.cpp
  658. src/util/statistics.cpp
  659. src/util/symbol.cpp
  660. src/util/timeit.cpp
  661. src/util/timeout.cpp
  662. src/util/timer.cpp
  663. src/util/trace.cpp
  664. src/util/util.cpp
  665. src/util/warning.cpp
  666. src/util/z3_exception.cpp
  667. g++ -o z3 shell/datalog_frontend.o shell/dimacs_frontend.o shell/gparams_register_modules.o shell/install_tactic.o shell/main.o shell/mem_initializer.o shell/smtlib_frontend.o shell/z3_log_frontend.o api/api.a parsers/smt/smtparser.a tactic/portfolio/portfolio.a tactic/ufbv/ufbv_tactic.a tactic/smtlogics/smtlogic_tactics.a muz_qe/muz_qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/fpa/fpa.a tactic/bv/bv_tactics.a smt/user_plugin/user_plugin.a smt/smt.a smt/proto_model/proto_model.a smt/params/smt_params.a ast/rewriter/bit_blaster/bit_blaster.a ast/pattern/pattern.a ast/macros/macros.a ast/simplifier/simplifier.a ast/proof_checker/proof_checker.a parsers/smt2/smt2parser.a cmd_context/extra_cmds/extra_cmds.a cmd_context/cmd_context.a solver/solver.a tactic/aig/aig_tactic.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a tactic/arith/arith_tactics.a sat/tactic/sat_tactic.a tactic/core/core_tactics.a math/euclid/euclid.a math/grobner/grobner.a parsers/util/parser_util.a ast/substitution/substitution.a tactic/tactic.a model/model.a ast/normal_forms/normal_forms.a ast/rewriter/rewriter.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/interval/interval.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/util.a -lpthread -fopenmp
  668. src/api/dll/dll.cpp
  669. src/api/dll/gparams_register_modules.cpp
  670. src/api/dll/install_tactic.cpp
  671. src/api/dll/mem_initializer.cpp
  672. g++ -o libz3.dylib -dynamiclib api/dll/dll.o api/dll/gparams_register_modules.o api/dll/install_tactic.o api/dll/mem_initializer.o api/api_algebraic.o api/api_arith.o api/api_array.o api/api_ast.o api/api_ast_map.o api/api_ast_vector.o api/api_bv.o api/api_commands.o api/api_config_params.o api/api_context.o api/api_datalog.o api/api_datatype.o api/api_goal.o api/api_log.o api/api_log_macros.o api/api_model.o api/api_numeral.o api/api_params.o api/api_parsers.o api/api_polynomial.o api/api_quant.o api/api_rcf.o api/api_solver.o api/api_solver_old.o api/api_stats.o api/api_tactic.o api/api_user_theory.o api/z3_replayer.o parsers/smt/smtparser.a tactic/portfolio/portfolio.a tactic/ufbv/ufbv_tactic.a tactic/smtlogics/smtlogic_tactics.a muz_qe/muz_qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/fpa/fpa.a tactic/bv/bv_tactics.a smt/user_plugin/user_plugin.a smt/smt.a smt/proto_model/proto_model.a smt/params/smt_params.a ast/rewriter/bit_blaster/bit_blaster.a ast/pattern/pattern.a ast/macros/macros.a ast/simplifier/simplifier.a ast/proof_checker/proof_checker.a parsers/smt2/smt2parser.a cmd_context/extra_cmds/extra_cmds.a cmd_context/cmd_context.a solver/solver.a tactic/aig/aig_tactic.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a tactic/arith/arith_tactics.a sat/tactic/sat_tactic.a tactic/core/core_tactics.a math/euclid/euclid.a math/grobner/grobner.a parsers/util/parser_util.a ast/substitution/substitution.a tactic/tactic.a model/model.a ast/normal_forms/normal_forms.a ast/rewriter/rewriter.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/interval/interval.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/util.a -fopenmp
  673. Z3 was successfully built.
  674. Z3Py scripts can already be executed in the 'build' directory.
  675. Z3Py scripts stored in arbitrary directories can be also executed if 'build' directory is added to the PYTHONPATH environment variable.
  676. Use the following command to install Z3 at prefix /Library.
  677. sudo make install
  678. Mukeshs-MacBook-Pro:build mukeshtiwari$ ls
  679. Makefile config.mk model sat tactic z3.py z3core.py z3poly.py z3rcf.py z3types.py
  680. api example.py muz_qe shell test z3.pyc z3core.pyc z3poly.pyc z3rcf.pyc z3types.pyc
  681. ast libz3.dylib nlsat smt util z3consts.py z3num.py z3printer.py z3test.py
  682. cmd_context math parsers solver z3 z3consts.pyc z3num.pyc z3printer.pyc z3test.pyc
  683. Mukeshs-MacBook-Pro:build mukeshtiwari$ pwd
  684. /Users/mukeshtiwari/SMT/z3/build
  685. Mukeshs-MacBook-Pro:build mukeshtiwari$ sudo make install
  686. Password:
  687. Z3 was successfully installed.
  688. Mukeshs-MacBook-Pro:build mukeshtiwari$
  689.  
  690. Mukeshs-MacBook-Pro:site-packages mukeshtiwari$ cabal install sbv --reinstall
  691. Warning: The package list for 'hackage.haskell.org' is 33 days old.
  692. Run 'cabal update' to get the latest list of available packages.
  693. Resolving dependencies...
  694. In order, the following will be installed:
  695. sbv-2.10 (reinstall) changes: HUnit-1.2.5.1 added
  696. Warning: Note that reinstalls are always dangerous. Continuing anyway...
  697. Configuring sbv-2.10...
  698. Building sbv-2.10...
  699. Preprocessing library sbv-2.10...
  700. [ 1 of 60] Compiling Data.SBV.Utils.TDiff ( Data/SBV/Utils/TDiff.hs, dist/build/Data/SBV/Utils/TDiff.o )
  701. [ 2 of 60] Compiling Data.SBV.Utils.Lib ( Data/SBV/Utils/Lib.hs, dist/build/Data/SBV/Utils/Lib.o )
  702. [ 3 of 60] Compiling Data.SBV.Utils.Boolean ( Data/SBV/Utils/Boolean.hs, dist/build/Data/SBV/Utils/Boolean.o )
  703. [ 4 of 60] Compiling Data.SBV.BitVectors.AlgReals ( Data/SBV/BitVectors/AlgReals.hs, dist/build/Data/SBV/BitVectors/AlgReals.o )
  704. [ 5 of 60] Compiling Data.SBV.BitVectors.Data ( Data/SBV/BitVectors/Data.hs, dist/build/Data/SBV/BitVectors/Data.o )
  705. [ 6 of 60] Compiling Data.SBV.Compilers.CodeGen ( Data/SBV/Compilers/CodeGen.hs, dist/build/Data/SBV/Compilers/CodeGen.o )
  706. [ 7 of 60] Compiling Data.SBV.Tools.ExpectedValue ( Data/SBV/Tools/ExpectedValue.hs, dist/build/Data/SBV/Tools/ExpectedValue.o )
  707. [ 8 of 60] Compiling Data.SBV.SMT.SMTLib1 ( Data/SBV/SMT/SMTLib1.hs, dist/build/Data/SBV/SMT/SMTLib1.o )
  708. [ 9 of 60] Compiling Data.SBV.BitVectors.Model ( Data/SBV/BitVectors/Model.hs, dist/build/Data/SBV/BitVectors/Model.o )
  709. Loading package ghc-prim ... linking ... done.
  710. Loading package integer-gmp ... linking ... done.
  711. Loading package base ... linking ... done.
  712. Loading package syb-0.3.7 ... linking ... done.
  713. Loading package array-0.4.0.1 ... linking ... done.
  714. Loading package deepseq-1.3.0.1 ... linking ... done.
  715. Loading package filepath-1.3.0.1 ... linking ... done.
  716. Loading package old-locale-1.0.0.5 ... linking ... done.
  717. Loading package time-1.4.0.1 ... linking ... done.
  718. Loading package bytestring-0.10.0.0 ... linking ... done.
  719. Loading package unix-2.6.0.0 ... linking ... done.
  720. Loading package directory-1.2.0.0 ... linking ... done.
  721. Loading package process-1.1.0.2 ... linking ... done.
  722. Loading package old-time-1.1.0.1 ... linking ... done.
  723. Loading package transformers-0.3.0.0 ... linking ... done.
  724. Loading package mtl-2.1.2 ... linking ... done.
  725. Loading package random-1.0.1.1 ... linking ... done.
  726. Loading package containers-0.5.0.0 ... linking ... done.
  727. Loading package pretty-1.1.1.0 ... linking ... done.
  728. Loading package template-haskell ... linking ... done.
  729. Loading package QuickCheck-2.5.1.1 ... linking ... done.
  730. [10 of 60] Compiling Data.SBV.BitVectors.PrettyNum ( Data/SBV/BitVectors/PrettyNum.hs, dist/build/Data/SBV/BitVectors/PrettyNum.o )
  731. [11 of 60] Compiling Data.SBV.BitVectors.SignCast ( Data/SBV/BitVectors/SignCast.hs, dist/build/Data/SBV/BitVectors/SignCast.o )
  732. [12 of 60] Compiling Data.SBV.BitVectors.Splittable ( Data/SBV/BitVectors/Splittable.hs, dist/build/Data/SBV/BitVectors/Splittable.o )
  733. [13 of 60] Compiling Data.SBV.BitVectors.STree ( Data/SBV/BitVectors/STree.hs, dist/build/Data/SBV/BitVectors/STree.o )
  734. [14 of 60] Compiling Data.SBV.Tools.Polynomial ( Data/SBV/Tools/Polynomial.hs, dist/build/Data/SBV/Tools/Polynomial.o )
  735. [15 of 60] Compiling Data.SBV.Compilers.C ( Data/SBV/Compilers/C.hs, dist/build/Data/SBV/Compilers/C.o )
  736. [16 of 60] Compiling Data.SBV.Internals ( Data/SBV/Internals.hs, dist/build/Data/SBV/Internals.o )
  737. [17 of 60] Compiling Data.SBV.Tools.GenTest ( Data/SBV/Tools/GenTest.hs, dist/build/Data/SBV/Tools/GenTest.o )
  738. [18 of 60] Compiling Data.SBV.SMT.SMT ( Data/SBV/SMT/SMT.hs, dist/build/Data/SBV/SMT/SMT.o )
  739. [19 of 60] Compiling Data.SBV.Provers.SExpr ( Data/SBV/Provers/SExpr.hs, dist/build/Data/SBV/Provers/SExpr.o )
  740. [20 of 60] Compiling Data.SBV.SMT.SMTLib2 ( Data/SBV/SMT/SMTLib2.hs, dist/build/Data/SBV/SMT/SMTLib2.o )
  741. [21 of 60] Compiling Data.SBV.SMT.SMTLib ( Data/SBV/SMT/SMTLib.hs, dist/build/Data/SBV/SMT/SMTLib.o )
  742. [22 of 60] Compiling Data.SBV.Provers.Yices ( Data/SBV/Provers/Yices.hs, dist/build/Data/SBV/Provers/Yices.o )
  743. [23 of 60] Compiling Data.SBV.Provers.Boolector ( Data/SBV/Provers/Boolector.hs, dist/build/Data/SBV/Provers/Boolector.o )
  744. [24 of 60] Compiling Data.SBV.Provers.CVC4 ( Data/SBV/Provers/CVC4.hs, dist/build/Data/SBV/Provers/CVC4.o )
  745. [25 of 60] Compiling Data.SBV.Provers.Z3 ( Data/SBV/Provers/Z3.hs, dist/build/Data/SBV/Provers/Z3.o )
  746. [26 of 60] Compiling Data.SBV.Provers.Prover ( Data/SBV/Provers/Prover.hs, dist/build/Data/SBV/Provers/Prover.o )
  747. [27 of 60] Compiling Data.SBV.Tools.Optimize ( Data/SBV/Tools/Optimize.hs, dist/build/Data/SBV/Tools/Optimize.o )
  748. [28 of 60] Compiling Data.SBV ( Data/SBV.hs, dist/build/Data/SBV.o )
  749. [29 of 60] Compiling Data.SBV.Bridge.Boolector ( Data/SBV/Bridge/Boolector.hs, dist/build/Data/SBV/Bridge/Boolector.o )
  750. [30 of 60] Compiling Data.SBV.Bridge.CVC4 ( Data/SBV/Bridge/CVC4.hs, dist/build/Data/SBV/Bridge/CVC4.o )
  751. [31 of 60] Compiling Data.SBV.Bridge.Yices ( Data/SBV/Bridge/Yices.hs, dist/build/Data/SBV/Bridge/Yices.o )
  752. [32 of 60] Compiling Data.SBV.Bridge.Z3 ( Data/SBV/Bridge/Z3.hs, dist/build/Data/SBV/Bridge/Z3.o )
  753. [33 of 60] Compiling Data.SBV.Examples.BitPrecise.BitTricks ( Data/SBV/Examples/BitPrecise/BitTricks.hs, dist/build/Data/SBV/Examples/BitPrecise/BitTricks.o )
  754. [34 of 60] Compiling Data.SBV.Examples.BitPrecise.Legato ( Data/SBV/Examples/BitPrecise/Legato.hs, dist/build/Data/SBV/Examples/BitPrecise/Legato.o )
  755. [35 of 60] Compiling Data.SBV.Examples.BitPrecise.MergeSort ( Data/SBV/Examples/BitPrecise/MergeSort.hs, dist/build/Data/SBV/Examples/BitPrecise/MergeSort.o )
  756. [36 of 60] Compiling Data.SBV.Examples.BitPrecise.PrefixSum ( Data/SBV/Examples/BitPrecise/PrefixSum.hs, dist/build/Data/SBV/Examples/BitPrecise/PrefixSum.o )
  757. [37 of 60] Compiling Data.SBV.Examples.CodeGeneration.AddSub ( Data/SBV/Examples/CodeGeneration/AddSub.hs, dist/build/Data/SBV/Examples/CodeGeneration/AddSub.o )
  758. [38 of 60] Compiling Data.SBV.Examples.CodeGeneration.CRC_USB5 ( Data/SBV/Examples/CodeGeneration/CRC_USB5.hs, dist/build/Data/SBV/Examples/CodeGeneration/CRC_USB5.o )
  759. [39 of 60] Compiling Data.SBV.Examples.CodeGeneration.Fibonacci ( Data/SBV/Examples/CodeGeneration/Fibonacci.hs, dist/build/Data/SBV/Examples/CodeGeneration/Fibonacci.o )
  760. [40 of 60] Compiling Data.SBV.Examples.CodeGeneration.GCD ( Data/SBV/Examples/CodeGeneration/GCD.hs, dist/build/Data/SBV/Examples/CodeGeneration/GCD.o )
  761. [41 of 60] Compiling Data.SBV.Examples.CodeGeneration.PopulationCount ( Data/SBV/Examples/CodeGeneration/PopulationCount.hs, dist/build/Data/SBV/Examples/CodeGeneration/PopulationCount.o )
  762. [42 of 60] Compiling Data.SBV.Examples.CodeGeneration.Uninterpreted ( Data/SBV/Examples/CodeGeneration/Uninterpreted.hs, dist/build/Data/SBV/Examples/CodeGeneration/Uninterpreted.o )
  763. [43 of 60] Compiling Data.SBV.Examples.Crypto.AES ( Data/SBV/Examples/Crypto/AES.hs, dist/build/Data/SBV/Examples/Crypto/AES.o )
  764. [44 of 60] Compiling Data.SBV.Examples.Crypto.RC4 ( Data/SBV/Examples/Crypto/RC4.hs, dist/build/Data/SBV/Examples/Crypto/RC4.o )
  765. [45 of 60] Compiling Data.SBV.Examples.Existentials.CRCPolynomial ( Data/SBV/Examples/Existentials/CRCPolynomial.hs, dist/build/Data/SBV/Examples/Existentials/CRCPolynomial.o )
  766. [46 of 60] Compiling Data.SBV.Examples.Existentials.Diophantine ( Data/SBV/Examples/Existentials/Diophantine.hs, dist/build/Data/SBV/Examples/Existentials/Diophantine.o )
  767. [47 of 60] Compiling Data.SBV.Examples.Polynomials.Polynomials ( Data/SBV/Examples/Polynomials/Polynomials.hs, dist/build/Data/SBV/Examples/Polynomials/Polynomials.o )
  768. [48 of 60] Compiling Data.SBV.Examples.Puzzles.Coins ( Data/SBV/Examples/Puzzles/Coins.hs, dist/build/Data/SBV/Examples/Puzzles/Coins.o )
  769. [49 of 60] Compiling Data.SBV.Examples.Puzzles.Counts ( Data/SBV/Examples/Puzzles/Counts.hs, dist/build/Data/SBV/Examples/Puzzles/Counts.o )
  770. [50 of 60] Compiling Data.SBV.Examples.Puzzles.DogCatMouse ( Data/SBV/Examples/Puzzles/DogCatMouse.hs, dist/build/Data/SBV/Examples/Puzzles/DogCatMouse.o )
  771. [51 of 60] Compiling Data.SBV.Examples.Puzzles.Euler185 ( Data/SBV/Examples/Puzzles/Euler185.hs, dist/build/Data/SBV/Examples/Puzzles/Euler185.o )
  772. [52 of 60] Compiling Data.SBV.Examples.Puzzles.MagicSquare ( Data/SBV/Examples/Puzzles/MagicSquare.hs, dist/build/Data/SBV/Examples/Puzzles/MagicSquare.o )
  773. [53 of 60] Compiling Data.SBV.Examples.Puzzles.NQueens ( Data/SBV/Examples/Puzzles/NQueens.hs, dist/build/Data/SBV/Examples/Puzzles/NQueens.o )
  774. [54 of 60] Compiling Data.SBV.Examples.Puzzles.Sudoku ( Data/SBV/Examples/Puzzles/Sudoku.hs, dist/build/Data/SBV/Examples/Puzzles/Sudoku.o )
  775. [55 of 60] Compiling Data.SBV.Examples.Puzzles.U2Bridge ( Data/SBV/Examples/Puzzles/U2Bridge.hs, dist/build/Data/SBV/Examples/Puzzles/U2Bridge.o )
  776. [56 of 60] Compiling Data.SBV.Examples.Uninterpreted.AUF ( Data/SBV/Examples/Uninterpreted/AUF.hs, dist/build/Data/SBV/Examples/Uninterpreted/AUF.o )
  777. [57 of 60] Compiling Data.SBV.Examples.Uninterpreted.Deduce ( Data/SBV/Examples/Uninterpreted/Deduce.hs, dist/build/Data/SBV/Examples/Uninterpreted/Deduce.o )
  778. [58 of 60] Compiling Data.SBV.Examples.Uninterpreted.Function ( Data/SBV/Examples/Uninterpreted/Function.hs, dist/build/Data/SBV/Examples/Uninterpreted/Function.o )
  779. [59 of 60] Compiling Data.SBV.Examples.Uninterpreted.Shannon ( Data/SBV/Examples/Uninterpreted/Shannon.hs, dist/build/Data/SBV/Examples/Uninterpreted/Shannon.o )
  780. [60 of 60] Compiling Data.SBV.Examples.Uninterpreted.Sort ( Data/SBV/Examples/Uninterpreted/Sort.hs, dist/build/Data/SBV/Examples/Uninterpreted/Sort.o )
  781. In-place registering sbv-2.10...
  782. Preprocessing executable 'SBVUnitTests' for sbv-2.10...
  783. [ 1 of 61] Compiling Examples.Arrays.Memory ( SBVUnitTest/Examples/Arrays/Memory.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/Examples/Arrays/Memory.o )
  784. [ 2 of 61] Compiling Examples.Basics.BasicTests ( SBVUnitTest/Examples/Basics/BasicTests.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/Examples/Basics/BasicTests.o )
  785. [ 3 of 61] Compiling Examples.Basics.Higher ( SBVUnitTest/Examples/Basics/Higher.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/Examples/Basics/Higher.o )
  786. [ 4 of 61] Compiling Examples.Basics.ProofTests ( SBVUnitTest/Examples/Basics/ProofTests.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/Examples/Basics/ProofTests.o )
  787. [ 5 of 61] Compiling Examples.Basics.QRem ( SBVUnitTest/Examples/Basics/QRem.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/Examples/Basics/QRem.o )
  788. [ 6 of 61] Compiling Examples.CRC.CCITT ( SBVUnitTest/Examples/CRC/CCITT.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/Examples/CRC/CCITT.o )
  789. Loading package ghc-prim ... linking ... done.
  790. Loading package integer-gmp ... linking ... done.
  791. Loading package base ... linking ... done.
  792. Loading package array-0.4.0.1 ... linking ... done.
  793. Loading package deepseq-1.3.0.1 ... linking ... done.
  794. Loading package old-locale-1.0.0.5 ... linking ... done.
  795. Loading package time-1.4.0.1 ... linking ... done.
  796. Loading package random-1.0.1.1 ... linking ... done.
  797. Loading package containers-0.5.0.0 ... linking ... done.
  798. Loading package pretty-1.1.1.0 ... linking ... done.
  799. Loading package template-haskell ... linking ... done.
  800. Loading package QuickCheck-2.5.1.1 ... linking ... done.
  801. Loading package filepath-1.3.0.1 ... linking ... done.
  802. Loading package bytestring-0.10.0.0 ... linking ... done.
  803. Loading package unix-2.6.0.0 ... linking ... done.
  804. Loading package directory-1.2.0.0 ... linking ... done.
  805. Loading package transformers-0.3.0.0 ... linking ... done.
  806. Loading package mtl-2.1.2 ... linking ... done.
  807. Loading package old-time-1.1.0.1 ... linking ... done.
  808. Loading package process-1.1.0.2 ... linking ... done.
  809. Loading package syb-0.3.7 ... linking ... done.
  810. Loading package sbv-2.10 ... linking ... done.
  811. Loading package HUnit-1.2.5.1 ... linking ... done.
  812. [ 7 of 61] Compiling Examples.CRC.CCITT_Unidir ( SBVUnitTest/Examples/CRC/CCITT_Unidir.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/Examples/CRC/CCITT_Unidir.o )
  813. [ 8 of 61] Compiling Examples.CRC.GenPoly ( SBVUnitTest/Examples/CRC/GenPoly.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/Examples/CRC/GenPoly.o )
  814. [ 9 of 61] Compiling Examples.CRC.Parity ( SBVUnitTest/Examples/CRC/Parity.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/Examples/CRC/Parity.o )
  815. [10 of 61] Compiling Examples.CRC.USB5 ( SBVUnitTest/Examples/CRC/USB5.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/Examples/CRC/USB5.o )
  816. [11 of 61] Compiling Examples.Puzzles.PowerSet ( SBVUnitTest/Examples/Puzzles/PowerSet.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/Examples/Puzzles/PowerSet.o )
  817. [12 of 61] Compiling Examples.Puzzles.Temperature ( SBVUnitTest/Examples/Puzzles/Temperature.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/Examples/Puzzles/Temperature.o )
  818. [13 of 61] Compiling Examples.Uninterpreted.Uninterpreted ( SBVUnitTest/Examples/Uninterpreted/Uninterpreted.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/Examples/Uninterpreted/Uninterpreted.o )
  819. [14 of 61] Compiling SBVUnitTestBuildTime ( SBVUnitTest/SBVUnitTestBuildTime.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/SBVUnitTestBuildTime.o )
  820. [15 of 61] Compiling Paths_sbv ( dist/build/autogen/Paths_sbv.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/Paths_sbv.o )
  821. [16 of 61] Compiling SBVTest ( SBVUnitTest/SBVTest.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/SBVTest.o )
  822. [17 of 61] Compiling TestSuite.Arrays.Memory ( SBVUnitTest/TestSuite/Arrays/Memory.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Arrays/Memory.o )
  823. [18 of 61] Compiling TestSuite.Basics.ArithNoSolver ( SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Basics/ArithNoSolver.o )
  824. [19 of 61] Compiling TestSuite.Basics.ArithSolver ( SBVUnitTest/TestSuite/Basics/ArithSolver.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Basics/ArithSolver.o )
  825. [20 of 61] Compiling TestSuite.Basics.BasicTests ( SBVUnitTest/TestSuite/Basics/BasicTests.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Basics/BasicTests.o )
  826. [21 of 61] Compiling TestSuite.Basics.Higher ( SBVUnitTest/TestSuite/Basics/Higher.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Basics/Higher.o )
  827. [22 of 61] Compiling TestSuite.Basics.ProofTests ( SBVUnitTest/TestSuite/Basics/ProofTests.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Basics/ProofTests.o )
  828. [23 of 61] Compiling TestSuite.Basics.QRem ( SBVUnitTest/TestSuite/Basics/QRem.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Basics/QRem.o )
  829. [24 of 61] Compiling TestSuite.BitPrecise.BitTricks ( SBVUnitTest/TestSuite/BitPrecise/BitTricks.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/BitPrecise/BitTricks.o )
  830. [25 of 61] Compiling TestSuite.BitPrecise.Legato ( SBVUnitTest/TestSuite/BitPrecise/Legato.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/BitPrecise/Legato.o )
  831. [26 of 61] Compiling TestSuite.BitPrecise.MergeSort ( SBVUnitTest/TestSuite/BitPrecise/MergeSort.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/BitPrecise/MergeSort.o )
  832. [27 of 61] Compiling TestSuite.BitPrecise.PrefixSum ( SBVUnitTest/TestSuite/BitPrecise/PrefixSum.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/BitPrecise/PrefixSum.o )
  833. [28 of 61] Compiling TestSuite.CRC.CCITT ( SBVUnitTest/TestSuite/CRC/CCITT.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/CRC/CCITT.o )
  834. [29 of 61] Compiling TestSuite.CRC.CCITT_Unidir ( SBVUnitTest/TestSuite/CRC/CCITT_Unidir.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/CRC/CCITT_Unidir.o )
  835. [30 of 61] Compiling TestSuite.CRC.GenPoly ( SBVUnitTest/TestSuite/CRC/GenPoly.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/CRC/GenPoly.o )
  836. [31 of 61] Compiling TestSuite.CRC.Parity ( SBVUnitTest/TestSuite/CRC/Parity.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/CRC/Parity.o )
  837. [32 of 61] Compiling TestSuite.CRC.USB5 ( SBVUnitTest/TestSuite/CRC/USB5.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/CRC/USB5.o )
  838. [33 of 61] Compiling TestSuite.CodeGeneration.AddSub ( SBVUnitTest/TestSuite/CodeGeneration/AddSub.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/CodeGeneration/AddSub.o )
  839. [34 of 61] Compiling TestSuite.CodeGeneration.CgTests ( SBVUnitTest/TestSuite/CodeGeneration/CgTests.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/CodeGeneration/CgTests.o )
  840. [35 of 61] Compiling TestSuite.CodeGeneration.CRC_USB5 ( SBVUnitTest/TestSuite/CodeGeneration/CRC_USB5.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/CodeGeneration/CRC_USB5.o )
  841. [36 of 61] Compiling TestSuite.CodeGeneration.Fibonacci ( SBVUnitTest/TestSuite/CodeGeneration/Fibonacci.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/CodeGeneration/Fibonacci.o )
  842. [37 of 61] Compiling TestSuite.CodeGeneration.GCD ( SBVUnitTest/TestSuite/CodeGeneration/GCD.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/CodeGeneration/GCD.o )
  843. [38 of 61] Compiling TestSuite.CodeGeneration.PopulationCount ( SBVUnitTest/TestSuite/CodeGeneration/PopulationCount.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/CodeGeneration/PopulationCount.o )
  844. [39 of 61] Compiling TestSuite.CodeGeneration.Uninterpreted ( SBVUnitTest/TestSuite/CodeGeneration/Uninterpreted.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/CodeGeneration/Uninterpreted.o )
  845. [40 of 61] Compiling TestSuite.Crypto.AES ( SBVUnitTest/TestSuite/Crypto/AES.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Crypto/AES.o )
  846. [41 of 61] Compiling TestSuite.Crypto.RC4 ( SBVUnitTest/TestSuite/Crypto/RC4.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Crypto/RC4.o )
  847. [42 of 61] Compiling TestSuite.Existentials.CRCPolynomial ( SBVUnitTest/TestSuite/Existentials/CRCPolynomial.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Existentials/CRCPolynomial.o )
  848. [43 of 61] Compiling TestSuite.Polynomials.Polynomials ( SBVUnitTest/TestSuite/Polynomials/Polynomials.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Polynomials/Polynomials.o )
  849. [44 of 61] Compiling TestSuite.Puzzles.Coins ( SBVUnitTest/TestSuite/Puzzles/Coins.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Puzzles/Coins.o )
  850. [45 of 61] Compiling TestSuite.Puzzles.Counts ( SBVUnitTest/TestSuite/Puzzles/Counts.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Puzzles/Counts.o )
  851. [46 of 61] Compiling TestSuite.Puzzles.DogCatMouse ( SBVUnitTest/TestSuite/Puzzles/DogCatMouse.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Puzzles/DogCatMouse.o )
  852. [47 of 61] Compiling TestSuite.Puzzles.Euler185 ( SBVUnitTest/TestSuite/Puzzles/Euler185.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Puzzles/Euler185.o )
  853. [48 of 61] Compiling TestSuite.Puzzles.MagicSquare ( SBVUnitTest/TestSuite/Puzzles/MagicSquare.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Puzzles/MagicSquare.o )
  854. [49 of 61] Compiling TestSuite.Puzzles.NQueens ( SBVUnitTest/TestSuite/Puzzles/NQueens.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Puzzles/NQueens.o )
  855. [50 of 61] Compiling TestSuite.Puzzles.PowerSet ( SBVUnitTest/TestSuite/Puzzles/PowerSet.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Puzzles/PowerSet.o )
  856. [51 of 61] Compiling TestSuite.Puzzles.Sudoku ( SBVUnitTest/TestSuite/Puzzles/Sudoku.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Puzzles/Sudoku.o )
  857. [52 of 61] Compiling TestSuite.Puzzles.Temperature ( SBVUnitTest/TestSuite/Puzzles/Temperature.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Puzzles/Temperature.o )
  858. [53 of 61] Compiling TestSuite.Puzzles.U2Bridge ( SBVUnitTest/TestSuite/Puzzles/U2Bridge.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Puzzles/U2Bridge.o )
  859. [54 of 61] Compiling TestSuite.Uninterpreted.AUF ( SBVUnitTest/TestSuite/Uninterpreted/AUF.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Uninterpreted/AUF.o )
  860. [55 of 61] Compiling TestSuite.Uninterpreted.Axioms ( SBVUnitTest/TestSuite/Uninterpreted/Axioms.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Uninterpreted/Axioms.o )
  861. [56 of 61] Compiling TestSuite.Uninterpreted.Function ( SBVUnitTest/TestSuite/Uninterpreted/Function.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Uninterpreted/Function.o )
  862. [57 of 61] Compiling TestSuite.Uninterpreted.Uninterpreted ( SBVUnitTest/TestSuite/Uninterpreted/Uninterpreted.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Uninterpreted/Uninterpreted.o )
  863. [58 of 61] Compiling Examples.Basics.Index ( SBVUnitTest/Examples/Basics/Index.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/Examples/Basics/Index.o )
  864. [59 of 61] Compiling TestSuite.Basics.Index ( SBVUnitTest/TestSuite/Basics/Index.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/TestSuite/Basics/Index.o )
  865. [60 of 61] Compiling SBVTestCollection ( SBVUnitTest/SBVTestCollection.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/SBVTestCollection.o )
  866. [61 of 61] Compiling Main ( SBVUnitTest/SBVUnitTest.hs, dist/build/SBVUnitTests/SBVUnitTests-tmp/Main.o )
  867. Linking dist/build/SBVUnitTests/SBVUnitTests ...
  868. Installing library in /Users/mukeshtiwari/.cabal/lib/sbv-2.10/ghc-7.6.1
  869. Installing executable(s) in /Users/mukeshtiwari/.cabal/bin
  870. Registering sbv-2.10...
  871. Installed sbv-2.10
  872.  
  873. Mukeshs-MacBook-Pro:site-packages mukeshtiwari$ ghci -XScopedTypeVariables
  874. GHCi, version 7.6.1: http://www.haskell.org/ghc/ :? for help
  875. Loading package ghc-prim ... linking ... done.
  876. Loading package integer-gmp ... linking ... done.
  877. Loading package base ... linking ... done.
  878. Prelude> :m Data.S
  879. Data.SBV Data.SBV.Examples.Puzzles.DogCatMouse Data.Semigroup.Traversable
  880. Data.SBV.Bridge.Boolector Data.SBV.Examples.Puzzles.Euler185 Data.Semigroupoid
  881. Data.SBV.Bridge.CVC4 Data.SBV.Examples.Puzzles.MagicSquare Data.Semigroupoid.Coproduct
  882. Data.SBV.Bridge.Yices Data.SBV.Examples.Puzzles.NQueens Data.Semigroupoid.Dual
  883. Data.SBV.Bridge.Z3 Data.SBV.Examples.Puzzles.Sudoku Data.Semigroupoid.Ob
  884. Data.SBV.Examples.BitPrecise.BitTricks Data.SBV.Examples.Puzzles.U2Bridge Data.Semigroupoid.Product
  885. Data.SBV.Examples.BitPrecise.Legato Data.SBV.Examples.Uninterpreted.AUF Data.Semigroupoid.Static
  886. Data.SBV.Examples.BitPrecise.MergeSort Data.SBV.Examples.Uninterpreted.Deduce Data.Sequence
  887. Data.SBV.Examples.BitPrecise.PrefixSum Data.SBV.Examples.Uninterpreted.Function Data.Sequence.Lens
  888. Data.SBV.Examples.CodeGeneration.AddSub Data.SBV.Examples.Uninterpreted.Shannon Data.Serialize
  889. Data.SBV.Examples.CodeGeneration.CRC_USB5 Data.SBV.Examples.Uninterpreted.Sort Data.Serialize.Builder
  890. Data.SBV.Examples.CodeGeneration.Fibonacci Data.SBV.Internals Data.Serialize.Get
  891. Data.SBV.Examples.CodeGeneration.GCD Data.STRef Data.Serialize.IEEE754
  892. Data.SBV.Examples.CodeGeneration.PopulationCount Data.STRef.Lazy Data.Serialize.Put
  893. Data.SBV.Examples.CodeGeneration.Uninterpreted Data.STRef.Strict Data.Set
  894. Data.SBV.Examples.Crypto.AES Data.Semifunctor Data.Set.Lens
  895. Data.SBV.Examples.Crypto.RC4 Data.Semifunctor.Associative Data.Stream
  896. Data.SBV.Examples.Existentials.CRCPolynomial Data.Semifunctor.Braided Data.String
  897. Data.SBV.Examples.Existentials.Diophantine Data.Semigroup Data.String.UTF8
  898. Data.SBV.Examples.Polynomials.Polynomials Data.Semigroup.Bifoldable Data.String.Utils
  899. Data.SBV.Examples.Puzzles.Coins Data.Semigroup.Bitraversable
  900. Data.SBV.Examples.Puzzles.Counts Data.Semigroup.Foldable
  901. Prelude> :m Data.SBV.Bridge.Z3
  902. Prelude Data.SBV.Bridge.Z3> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x
  903. Loading package pretty-1.1.1.0 ... linking ... done.
  904. Loading package array-0.4.0.1 ... linking ... done.
  905. Loading package deepseq-1.3.0.1 ... linking ... done.
  906. Loading package filepath-1.3.0.1 ... linking ... done.
  907. Loading package old-locale-1.0.0.5 ... linking ... done.
  908. Loading package time-1.4.0.1 ... linking ... done.
  909. Loading package bytestring-0.10.0.0 ... linking ... done.
  910. Loading package unix-2.6.0.0 ... linking ... done.
  911. Loading package directory-1.2.0.0 ... linking ... done.
  912. Loading package process-1.1.0.2 ... linking ... done.
  913. Loading package old-time-1.1.0.1 ... linking ... done.
  914. Loading package containers-0.5.0.0 ... linking ... done.
  915. Loading package random-1.0.1.1 ... linking ... done.
  916. Loading package template-haskell ... linking ... done.
  917. Loading package QuickCheck-2.5.1.1 ... linking ... done.
  918. Loading package transformers-0.3.0.0 ... linking ... done.
  919. Loading package mtl-2.1.2 ... linking ... done.
  920. Loading package syb-0.3.7 ... linking ... done.
  921. Loading package sbv-2.10 ... linking ... done.
  922. *** An error occurred.
  923. *** Unable to locate executable for z3
  924. *** Executable specified: "z3"
  925. Prelude Data.SBV.Bridge.Z3>
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement
Public Pastes
Advertisement
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!