From 1850879e7e196c0e1c00900acf5facaaf5387beb Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 18 Sep 2023 10:55:13 +0100
Subject: Add benchmarking of unhashed commands

---
 src/extraction/Extraction.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'src/extraction')

diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index 0a83f02..cd8b037 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -28,6 +28,8 @@ From vericert Require
      HLSOpts
      Predicate
      Bourdoncle
+     GiblePargenproofEquiv
+     GiblePargen
 .
 
 From Coq Require DecidableClass.
@@ -209,7 +211,8 @@ Separate Extraction
          Verilog.stmnt_to_list
          Bourdoncle.bourdoncle
 
-   Smtpredicate.check_smt_total
+   Smtpredicate.check_smt_total GiblePargenproofEquiv.check GiblePargen.check_evaluability1
+   GiblePargen.check_evaluability2
 
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
-- 
cgit