From b32e7574864cde80f8f5283431c21a6803a89108 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Thu, 10 Aug 2023 11:17:19 +0100 Subject: Fix backend hardware generation and scheduling --- driver/VericertDriver.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'driver') 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 -- cgit