Merge branch 'master' into btor-ng

10 files changed, 54 insertions, 9 deletions

diff --git a/.travis/setup.sh b/.travis/setup.sh
index 23bdf563f..81ff37742 100755
--- a/.travis/setup.sh
+++ b/.travis/setup.sh
@@ -29,8 +29,16 @@ fi
 if [ z"$TRAVIS_BRANCH" != z ]; then
 	TRAVIS_COMMIT_ACTUAL=$(git log --pretty=format:'%H' -n 1)
 	echo "- Fixing detached head (current $TRAVIS_COMMIT_ACTUAL -> $TRAVIS_COMMIT)"
-	git fetch origin $TRAVIS_COMMIT
+	git remote -v
 	git branch -v
+	if [ x"$(git show-ref -s HEAD)" = x"$TRAVIS_COMMIT" ]; then
+		echo "Checked out at $TRAVIS_COMMIT"
+	else
+		if [ z"$TRAVIS_PULL_REQUEST_SLUG" != z ]; then
+			git fetch source $TRAVIS_COMMIT || echo "Unable to fetch $TRAVIS_COMMIT from source"
+		fi
+		git fetch origin $TRAVIS_COMMIT || echo "Unable to fetch $TRAVIS_COMMIT from origin"
+	fi
 	git branch -D $TRAVIS_BRANCH || true
 	git checkout $TRAVIS_COMMIT -b $TRAVIS_BRANCH
 	git branch -v
diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc
index e0ee6292d..4be5fd493 100644
--- a/libs/ezsat/ezminisat.cc
+++ b/libs/ezsat/ezminisat.cc
@@ -18,8 +18,12 @@
  */
 
 // needed for MiniSAT headers (see Minisat Makefile)
-#define __STDC_LIMIT_MACROS
+#ifndef __STDC_FORMAT_MACROS
 #define __STDC_FORMAT_MACROS
+#endif
+#ifndef __STDC_LIMIT_MACROS
+#define __STDC_LIMIT_MACROS
+#endif
 
 #include "ezminisat.h"
 
diff --git a/libs/minisat/00_PATCH_remove_zlib.patch b/libs/minisat/00_PATCH_remove_zlib.patch
index 61a36f7e5..068356b73 100644
--- a/libs/minisat/00_PATCH_remove_zlib.patch
+++ b/libs/minisat/00_PATCH_remove_zlib.patch
@@ -36,3 +36,20 @@
  
      int  operator *  () const { return (pos >= size) ? EOF : buf[pos]; }
      void operator ++ ()       { pos++; assureLookahead(); }
+--- Dimacs.h
++++ Dimacs.h
+@@ -76,10 +76,10 @@ static void parse_DIMACS_main(B& in, Solver& S, bool strictp = false) {
+ 
+ // Inserts problem into solver.
+ //
+-template<class Solver>
+-static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) {
+-    StreamBuffer in(input_stream);
+-    parse_DIMACS_main(in, S, strictp); }
++//template<class Solver>
++//static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) {
++//    StreamBuffer in(input_stream);
++//    parse_DIMACS_main(in, S, strictp); }
+ 
+ //=================================================================================================
+ }
diff --git a/libs/minisat/00_UPDATE.sh b/libs/minisat/00_UPDATE.sh
index 2ffc11553..ea26215ab 100644..100755
--- a/libs/minisat/00_UPDATE.sh
+++ b/libs/minisat/00_UPDATE.sh
@@ -9,8 +9,8 @@ rm -rf minisat_upstream
 sed -i -e 's,^#include *"minisat/[^/]\+/\?,#include ",' *.cc *.h
 sed -i -e 's/Minisat::memUsedPeak()/Minisat::memUsedPeak(bool)/' System.cc
 sed -i -e 's/PRI[iu]64/ & /' Options.h Solver.cc
-sed -i -e '1 i #define __STDC_LIMIT_MACROS' *.cc
-sed -i -e '1 i #define __STDC_FORMAT_MACROS' *.cc
+sed -i -e '1 i #ifndef __STDC_LIMIT_MACROS\n#define __STDC_LIMIT_MACROS\n#endif' *.cc
+sed -i -e '1 i #ifndef __STDC_FORMAT_MACROS\n#define __STDC_FORMAT_MACROS\n#endif' *.cc
 
 patch -p0 < 00_PATCH_mkLit_default_arg.patch
 patch -p0 < 00_PATCH_remove_zlib.patch
diff --git a/libs/minisat/Dimacs.h b/libs/minisat/Dimacs.h
index ccfa1c013..61b9d3ca0 100644
--- a/libs/minisat/Dimacs.h
+++ b/libs/minisat/Dimacs.h
@@ -76,10 +76,10 @@ static void parse_DIMACS_main(B& in, Solver& S, bool strictp = false) {
 
 // Inserts problem into solver.
 //
-template<class Solver>
-static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) {
-    StreamBuffer in(input_stream);
-    parse_DIMACS_main(in, S, strictp); }
+//template<class Solver>
+//static void parse_DIMACS(gzFile input_stream, Solver& S, bool strictp = false) {
+//    StreamBuffer in(input_stream);
+//    parse_DIMACS_main(in, S, strictp); }
 
 //=================================================================================================
 }
diff --git a/libs/minisat/Options.cc b/libs/minisat/Options.cc
index 1aff3fab2..5c45dd6ac 100644
--- a/libs/minisat/Options.cc
+++ b/libs/minisat/Options.cc
@@ -1,5 +1,9 @@
+#ifndef __STDC_FORMAT_MACROS
 #define __STDC_FORMAT_MACROS
+#endif
+#ifndef __STDC_LIMIT_MACROS
 #define __STDC_LIMIT_MACROS
+#endif
 /**************************************************************************************[Options.cc]
 Copyright (c) 2008-2010, Niklas Sorensson
 
diff --git a/libs/minisat/SimpSolver.cc b/libs/minisat/SimpSolver.cc
index fd5774e0e..7348a905d 100644
--- a/libs/minisat/SimpSolver.cc
+++ b/libs/minisat/SimpSolver.cc
@@ -1,5 +1,9 @@
+#ifndef __STDC_FORMAT_MACROS
 #define __STDC_FORMAT_MACROS
+#endif
+#ifndef __STDC_LIMIT_MACROS
 #define __STDC_LIMIT_MACROS
+#endif
 /***********************************************************************************[SimpSolver.cc]
 Copyright (c) 2006,      Niklas Een, Niklas Sorensson
 Copyright (c) 2007-2010, Niklas Sorensson
diff --git a/libs/minisat/Solver.cc b/libs/minisat/Solver.cc
index ab476853a..f6d4fb5ae 100644
--- a/libs/minisat/Solver.cc
+++ b/libs/minisat/Solver.cc
@@ -1,5 +1,9 @@
+#ifndef __STDC_FORMAT_MACROS
 #define __STDC_FORMAT_MACROS
+#endif
+#ifndef __STDC_LIMIT_MACROS
 #define __STDC_LIMIT_MACROS
+#endif
 /***************************************************************************************[Solver.cc]
 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
 Copyright (c) 2007-2010, Niklas Sorensson
diff --git a/libs/minisat/System.cc b/libs/minisat/System.cc
index ceef4292b..1921a1d71 100644
--- a/libs/minisat/System.cc
+++ b/libs/minisat/System.cc
@@ -1,5 +1,9 @@
+#ifndef __STDC_FORMAT_MACROS
 #define __STDC_FORMAT_MACROS
+#endif
+#ifndef __STDC_LIMIT_MACROS
 #define __STDC_LIMIT_MACROS
+#endif
 /***************************************************************************************[System.cc]
 Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
 Copyright (c) 2007-2010, Niklas Sorensson
diff --git a/libs/subcircuit/subcircuit.h b/libs/subcircuit/subcircuit.h
index 5291c6421..8368efab1 100644
--- a/libs/subcircuit/subcircuit.h
+++ b/libs/subcircuit/subcircuit.h
@@ -131,7 +131,7 @@ namespace SubCircuit
 
 	public:
 		Solver();
-		~Solver();
+		virtual ~Solver();
 
 		void setVerbose();
 		void addGraph(std::string graphId, const Graph &graph);