From 1d86b1c178deb97f3d499f461a417a4fe6846cf8 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Wed, 20 Oct 2021 10:03:01 +0100
Subject: Start to prove termination of SAT

---
 src/hls/RTLBlockInstr.v | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'src/hls/RTLBlockInstr.v')

diff --git a/src/hls/RTLBlockInstr.v b/src/hls/RTLBlockInstr.v
index 5e17115..8353452 100644
--- a/src/hls/RTLBlockInstr.v
+++ b/src/hls/RTLBlockInstr.v
@@ -251,12 +251,6 @@ Definition sat_pred_simple (bound: nat) (p: pred_op) :=
   | None => None
   end.
 
-Definition sat_pred_temp (bound: nat) (p: pred_op) :=
-  match trans_pred_temp bound p with
-  | Some fm => boundedSatSimple bound fm
-  | None => None
-  end.
-
 Inductive instr : Type :=
 | RBnop : instr
 | RBop : option pred_op -> operation -> list reg -> reg -> instr
-- 
cgit