disable shrinking by default (causes SEGFAULTs)

CaDiCaL.vcxproj

@@ -38,6 +38,7 @@
     <UseDebugLibraries>false</UseDebugLibraries>
     <PlatformToolset>v143</PlatformToolset>
     <WholeProgramOptimization>true</WholeProgramOptimization>
+    <EnableASAN>false</EnableASAN>
   </PropertyGroup>
   <Import Project="$(VCTargetsPath)\Microsoft.Cpp.props" />
   <ImportGroup Label="ExtensionSettings">

src/clause.hpp

@@ -22,28 +22,29 @@ typedef const int * const_literal_iterator;
 // memory but more importantly also requires another memory access and thus
 // is very costly.
 
+#pragma pack(push, 1)
 struct Clause {
 #ifdef LOGGING
   int64_t id;         // Only useful for debugging.
 #endif
 
-  bool conditioned:1; // Tried for globally blocked clause elimination.
-  bool covered:1;     // Already considered for covered clause elimination.
-  bool enqueued:1;    // Enqueued on backward queue.
-  bool frozen:1;      // Temporarily frozen (in covered clause elimination).
-  bool garbage:1;     // can be garbage collected unless it is a 'reason'
-  bool gate:1 ;       // Clause part of a gate (function definition).
-  bool hyper:1;       // redundant hyper binary or ternary resolved
-  bool instantiated:1;// tried to instantiate
-  bool keep:1;        // always keep this clause (if redundant)
-  bool moved:1;       // moved during garbage collector ('copy' valid)
-  bool reason:1;      // reason / antecedent clause can not be collected
-  bool redundant:1;   // aka 'learned' so not 'irredundant' (original)
-  bool transred:1;    // already checked for transitive reduction
-  bool subsume:1;     // not checked in last subsumption round
+  unsigned conditioned:1; // Tried for globally blocked clause elimination.
+  unsigned covered:1;     // Already considered for covered clause elimination.
+  unsigned enqueued:1;    // Enqueued on backward queue.
+  unsigned frozen:1;      // Temporarily frozen (in covered clause elimination).
+  unsigned garbage:1;     // can be garbage collected unless it is a 'reason'
+  unsigned gate:1 ;       // Clause part of a gate (function definition).
+  unsigned hyper:1;       // redundant hyper binary or ternary resolved
+  unsigned instantiated:1;// tried to instantiate
+  unsigned keep:1;        // always keep this clause (if redundant)
+  unsigned moved:1;       // moved during garbage collector ('copy' valid)
+  unsigned reason:1;      // reason / antecedent clause can not be collected
+  unsigned redundant:1;   // aka 'learned' so not 'irredundant' (original)
+  unsigned transred:1;    // already checked for transitive reduction
+  unsigned subsume:1;     // not checked in last subsumption round
   unsigned used:2;    // resolved in conflict analysis since last 'reduce'
-  bool vivified:1;    // clause already vivified
-  bool vivify:1;      // clause scheduled to be vivified
+  unsigned vivified:1;    // clause already vivified
+  unsigned vivify:1;      // clause scheduled to be vivified
 
   // The glucose level ('LBD' or short 'glue') is a heuristic value for the
   // expected usefulness of a learned clause, where smaller glue is consider
@@ -131,6 +132,7 @@ struct clause_smaller_size {
     return a->size < b->size;
   }
 };
+#pragma pack(pop)
 
 /*------------------------------------------------------------------------*/
 

src/options.hpp

@@ -138,7 +138,7 @@ OPTION( reverse,           0,  0,  1,0,0,1, "reverse variable ordering") \
 OPTION( score,             1,  0,  1,0,0,1, "use EVSIDS scores") \
 OPTION( scorefactor,     950,500,1e3,0,0,1, "score factor per mille") \
 OPTION( seed,              0,  0,2e9,0,0,1, "random seed") \
-OPTION( shrink,            3,  0,  3,0,0,1, "shrink conflict clause") \
+OPTION( shrink,            0,  0,  3,0,0,1, "shrink conflict clause") \
 OPTION( shrinkreap,        1,  0,  1,0,0,1, "use a reap for shrinking") \
 OPTION( shuffle,           0,  0,  1,0,0,1, "shuffle variables") \
 OPTION( shufflequeue,      1,  0,  1,0,0,1, "shuffle variable queue") \