diff options
author | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 11:17:19 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 11:17:19 +0100 |
commit | b32e7574864cde80f8f5283431c21a6803a89108 (patch) | |
tree | f30babb0db7e5797cb77f6ac44a682cb9b8b105b /driver | |
parent | c321e39de166308d8db2f6ebe577edb3297b507c (diff) | |
download | vericert-b32e7574864cde80f8f5283431c21a6803a89108.tar.gz vericert-b32e7574864cde80f8f5283431c21a6803a89108.zip |
Fix backend hardware generation and scheduling
Diffstat (limited to 'driver')
-rw-r--r-- | driver/VericertDriver.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/driver/VericertDriver.ml b/driver/VericertDriver.ml index 87ce2c6..5950e95 100644 --- a/driver/VericertDriver.ml +++ b/driver/VericertDriver.ml @@ -98,7 +98,7 @@ let compile_c_file sourcename ifile ofile = then Vericert.Compiler0.transf_hls_temp else Vericert.Compiler0.transf_hls in - let _ = Vericert.Smtpredicate.check_smt (Vericert.Predicate0.Pimp ((Vericert.Predicate0.Pbase (Vericert.Camlcoq.P.of_int 2)),(Vericert.Predicate0.Pbase (Vericert.Camlcoq.P.of_int 2)))) in + (* let _ = Vericert.Smtpredicate.check_smt (Vericert.Predicate0.Pimp ((Vericert.Predicate0.Pbase (Vericert.Camlcoq.P.of_int 2)),(Vericert.Predicate0.Pbase (Vericert.Camlcoq.P.of_int 2)))) in *) match translation csyntax with | Vericert.Errors.OK v -> if !Vericert.Cohpred.cohpred_counter > 0 then Printf.fprintf stderr "OK\n"; v |