Commit 971f8332 authored by MARCHE Claude's avatar MARCHE Claude

The certified prover runs, at last

parent 7ac0d1f3
......@@ -34,15 +34,16 @@ CMX=$(patsubst %,%.cmx,$(ML))
CMI=$(patsubst %,%.cmi,$(ML))
OCAMLC=ocamlopt.opt
INCLUDES=-I $(BD) $(INCLUDE)
LIBS=nums.cmxa why3__BuiltIn.cmx int__Int.cmx array__Array.cmx
LIBS=$(BIGINTLIB).cmxa why3extract.cmxa
LIBSOLD=$(BD)/why3__BuiltIn.cmx $(BD)/int__Int.cmx $(BD)/array__Array.cmx
WHY3FLAGS=-L . --debug ignore_unused_vars --debug extraction
MLFLAGS=
MLIFLAGS=
MLEXECFLAGS=
$(BD)/prover: $(CMX) $(BD)/Prover.ml
echo $(OCAMLC) $(INCLUDES) $(LIBS) $(MLFLAGS) $(MLEXECFLAGS) \
-o $(BD)/prover $<
$(BD)/prover: $(CMX) run.cmx
$(OCAMLC) $(INCLUDES) $(LIBS) $(MLFLAGS) $(MLEXECFLAGS) \
-o $(BD)/prover $^
%.cmx: %.ml
$(OCAMLC) $(INCLUDES) $(MLFLAGS) -c $<
......
let n = Why3extract.Why3__BigInt.of_int
let () =
Format.eprintf "Running the test (zenon10 2)@.";
ProverMain__Impl.main (ProverTest__Impl.zenon10 (n 2)) (n 1);
Format.eprintf "Done (which means 'unsat')@."
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment