diff --git a/fstar-helpers/Makefile.base b/fstar-helpers/Makefile.base index 6eb4fc9cc..54c2552b1 100644 --- a/fstar-helpers/Makefile.base +++ b/fstar-helpers/Makefile.base @@ -10,5 +10,5 @@ EXTRA_HELPMESSAGE += printf "Libcrux specifics:\n"; EXTRA_HELPMESSAGE += target SLOW_MODULES 'a list of modules to verify fully only when `VERIFY_SLOW_MODULES` is set to `yes`. When `VERIFY_SLOW_MODULES`, those modules are admitted.'; EXTRA_HELPMESSAGE += target VERIFY_SLOW_MODULES '`yes` or `no`, defaults to `no`'; -FSTAR_INCLUDE_DIRS_EXTRA += $(HACL_HOME)/specs $(shell git rev-parse --show-toplevel)/fstar-helpers/fstar-bitvec +FSTAR_INCLUDE_DIRS_EXTRA += $(HACL_HOME)/specs include $(shell git rev-parse --show-toplevel)/fstar-helpers/Makefile.generic diff --git a/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti b/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti index e8713dad5..95dad6932 100644 --- a/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti +++ b/sys/platform/proofs/fstar/extraction/Libcrux_platform.Platform.fsti @@ -1,5 +1,5 @@ module Libcrux_platform.Platform -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +#set-options "--fuel 0 --ifuel 1 --z3rlimit 80" open Core open FStar.Mul