more datail from the build failure

diff --git a/.cproject b/.cproject
index 6145dec050b1208e957bc8d375da07e5e32adc71..6467c05f2e00f6df18220072ca1c8037c04fe5e5 100644 (file)
--- a/.cproject
+++ b/.cproject
@@ -326,6 +326,14 @@
                                <useDefaultCommand>true</useDefaultCommand>
                                <runAllBuilders>true</runAllBuilders>
                        </target>
+                       <target name="check" path="test/unit" targetID="org.eclipse.cdt.build.MakeTargetBuilder">
+                               <buildCommand>make</buildCommand>
+                               <buildArguments>-j10</buildArguments>
+                               <buildTarget>check</buildTarget>
+                               <stopOnError>true</stopOnError>
+                               <useDefaultCommand>true</useDefaultCommand>
+                               <runAllBuilders>true</runAllBuilders>
+                       </target>
                </buildTargets>
        </storageModule>
 </cproject>

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index d4e1234897b90c0c3f1006e167595ae70376209a..3d2d4c9eaf73944a408b04085b66623197cce075 100644 (file)
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -120,7 +120,7 @@ void MinisatSatSolver::renewVar(SatLiteral lit, int level) {
   Unreachable();
 }
 
-int MinisatSatSolver::getAssertionLevel() const {
+unsigned MinisatSatSolver::getAssertionLevel() const {
   // we have no user context implemented so far
   return 0;
 }

diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 7c12fcbd0cb384a2fec5cbd374f9eb39a84f024e..ed164904e96faedf72591bc7d947583048201271 100644 (file)
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -48,7 +48,7 @@ public:
 
   void unregisterVar(SatLiteral lit);
   void renewVar(SatLiteral lit, int level = -1);
-  int getAssertionLevel() const;
+  unsigned getAssertionLevel() const;
 
 
   // helper methods for converting from the internal Minisat representation

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index bc611a097fba4a74a072262a882f1a219fa508db..ede18c5854364efc799cb786ae5e00c5fc1d8574 100644 (file)
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -161,7 +161,7 @@ bool DPLLMinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) co
 
 /** Incremental interface */
 
-int DPLLMinisatSatSolver::getAssertionLevel() const {
+unsigned DPLLMinisatSatSolver::getAssertionLevel() const {
   return d_minisat->getAssertionLevel();
 }
 

diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 81a12c491e885934d9cdfd9bf4c5f44bb893bc38..dc06753ab5f962e4960c742162d1720959f09dc9 100644 (file)
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -69,7 +69,7 @@ public:
 
   /** Incremental interface */
 
-  int getAssertionLevel() const;
+  unsigned getAssertionLevel() const;
 
   void push();