From ba0d855fd4eed9439e4ce4fa6eb778cbb2250708 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 7 Sep 2017 19:16:13 -0700
Subject: Trying to enable CNF simplification in &bmcs -g.

---
 src/sat/bmc/bmc.h | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/sat/bmc/bmc.h')

diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 2585c773..8e249339 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -95,6 +95,7 @@ struct Bmc_AndPar_t_
     int         fUseSynth;      // use synthesis
     int         fUseOldCnf;     // use old CNF construction
     int         fUseGlucose;    // use Glucose 3.0 as the default solver
+    int         fUseEliminate;  // use variable elimination
     int         fVerbose;       // verbose 
     int         fVeryVerbose;   // very verbose 
     int         fNotVerbose;    // skip line-by-line print-out 
-- 
cgit v1.2.3