5 files changed, 10 insertions, 8 deletions
diff --git a/proofs/lfsc_checker/.gitignore b/proofs/lfsc_checker/.gitignore
index 1f799d15a..0712efe67 100644
--- a/proofs/lfsc_checker/.gitignore
+++ b/proofs/lfsc_checker/.gitignore
@@ -12,5 +12,4 @@ Makefile.in
 /aclocal.m4
 *~
 \#*\#
-/config/
 *.swp
diff --git a/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx.m4 b/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx.m4
new file mode 120000
index 000000000..0543a154f
--- /dev/null
+++ b/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx.m4
@@ -0,0 +1 @@
+../../../config/ax_cxx_compile_stdcxx.m4
+\ No newline at end of file
diff --git a/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx_11.m4 b/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx_11.m4
new file mode 120000
index 000000000..77adcd7a9
--- /dev/null
+++ b/proofs/lfsc_checker/config/ax_cxx_compile_stdcxx_11.m4
@@ -0,0 +1 @@
+../../../config/ax_cxx_compile_stdcxx_11.m4
+\ No newline at end of file
diff --git a/proofs/lfsc_checker/configure.ac b/proofs/lfsc_checker/configure.ac
index 5f4353664..9ef902237 100644
--- a/proofs/lfsc_checker/configure.ac
+++ b/proofs/lfsc_checker/configure.ac
@@ -27,6 +27,10 @@ AC_DISABLE_STATIC
 AC_PROG_CXX
 AC_PROG_CC
 
+# C++11 support in the compiler is now mandatory. Check for support and add
+# switches if necessary.
+AX_CXX_COMPILE_STDCXX_11([ext], [mandatory])
+
 # Checks for libraries.
 # FIXME: Replace `main' with a function in `-lgmp':
 AC_CHECK_LIB([gmp], [__gmpz_init])
diff --git a/proofs/lfsc_checker/expr.h b/proofs/lfsc_checker/expr.h
index 632aaa18a..0677533da 100644
--- a/proofs/lfsc_checker/expr.h
+++ b/proofs/lfsc_checker/expr.h
@@ -2,11 +2,12 @@
 #define sc2__expr_h
 
 #include <stdint.h>
-#include <ext/hash_set>
 #include <iostream>
 #include <map>
 #include <string>
+#include <unordered_set>
 #include <vector>
+
 #include "chunking_memory_management.h"
 #include "gmp.h"
 
@@ -57,21 +58,17 @@ enum { NOT_CEXPR = 0, // for INT_EXPR, HOLE_EXPR, SYM_EXPR, SYMS_EXPR
 class Expr;
 class SymExpr;
 
-namespace __gnu_cxx {
-template <>
-struct hash<Expr *> {
+struct hashExprPtr {
   size_t operator()(const Expr *x) const {
     return reinterpret_cast<uintptr_t>(x);
   }
 };
-}
 
 struct eqExprPtr {
   bool operator()(const Expr *e1, const Expr *e2) const { return e1 == e2; }
 };
 
-typedef __gnu_cxx::hash_set<Expr *, __gnu_cxx::hash<Expr *>, eqExprPtr>
-    expr_ptr_set_t;
+typedef std::unordered_set<Expr *, hashExprPtr, eqExprPtr> expr_ptr_set_t;
 
 class Expr {
 protected: