krpcannon

krpcannon

; Starting query at ./bloat5.fst(8,18-8,68)
(declare-fun label_2 () Bool)
(declare-fun label_1 () Bool)
(push)

; <fuel='2' ifuel='1'>
(assert (= MaxFuel
(SFuel (SFuel ZFuel))))
(assert (= MaxIFuel
(SFuel ZFuel)))

krpcannon

Keiths-MacBook-Pro:elpi Krpcannon$ make H=
Makefile:128: .depends: No such file or directory
Makefile:128: .depends.parser: No such file or directory
printf 'OCAMLDEP %-26s %s\n' ".depends.parser" ""
OCAMLDEP .depends.parser            
ocamlfind ocamldep -native -pp 'camlp5o -I . -I +camlp5 pa_extend.cmo pa_lexer.cmo' elpi_parser.ml > .depends.parser
printf 'OCAMLDEP %-26s %s\n' ".depends" ""
OCAMLDEP .depends                   
ocamlfind ocamldep -native elpi.ml elpi_API.ml elpi_ast.ml elpi_compiler.ml elpi_custom.ml elpi_data.ml elpi_latex_exporter.ml elpi_prolog_exporter.ml elpi_ptmap.ml elpi_runtime.ml elpi_trace.ml elpi_util.ml trace_ppx.ml elpi_API.mli elpi_ast.mli elpi_compiler.mli elpi_custom.mli elpi_latex_exporter.mli elpi_parser.mli elpi_prolog_exporter.mli elpi_ptmap.mli elpi_runtime.mli elpi_trace.mli elpi_util.mli > .depends
ocamlfind query camlp5 > /dev/null

krpcannon

; Starting query at ./bloat9.fst(7,31-9,24)
(declare-fun label_32 () Bool)
(push)

; <fuel='2' ifuel='1'>
(assert (= MaxFuel
(SFuel (SFuel ZFuel))))
(assert (= MaxIFuel
(SFuel ZFuel)))
;;;;;;;;;;;;;;;;query

krpcannon

; Starting query at ./simplefactorial.fst(1,22-4,61)
;;;;;;;;;;;;;;;;Uninterpreted function symbol for impure function
(declare-fun Simplefactorial.factorial (Term) Term)
;;;;;;;;;;;;;;;;Uninterpreted name for impure function
(declare-fun Simplefactorial.factorial@tok () Term)
(declare-fun label_34 () Bool)
(declare-fun label_33 () Bool)
(declare-fun label_32 () Bool)
(push)

krpcannon

; Starting query at ./bloat6.fst(5,29-8,68)
;;;;;;;;;;;;;;;;n#54 : Bloat6.nat (Bloat6.nat)
(declare-fun x_a42ae5f759af5bb08f7f27c259de7ecb_0 () Term)
;;;;;;;;;;;;;;;;binder_x_a42ae5f759af5bb08f7f27c259de7ecb_0
(assert (!
(HasType x_a42ae5f759af5bb08f7f27c259de7ecb_0
Bloat6.nat)
:named binder_x_a42ae5f759af5bb08f7f27c259de7ecb_0))
(declare-fun Tm_refine_132efab4ca0e1877b81a374a0ce191e7 (Term) Term)
;;;;;;;;;;;;;;;;refinement kinding