diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2023-08-10 11:17:19 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2023-08-11 17:15:39 +0100 |
| commit | 6ad3f69cf04d0055b7987e6e4c858a64d3b1693c (patch) | |
| tree | c686b80ee30c1280f005c27d60a6344bbee8d646 /driver | |
| parent | 05afcff334725e885522e9859b9ab735a404014c (diff) | |
| download | vericert-6ad3f69cf04d0055b7987e6e4c858a64d3b1693c.tar.gz vericert-6ad3f69cf04d0055b7987e6e4c858a64d3b1693c.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 |