From 79f1d7b4d40781932c44aaaa31f13d9ce7e1865f Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Mon, 24 Oct 2016 15:27:47 +0100
Subject: [PATCH] fixed GCC build issue in tests

---
 src/test/sorting_network.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/test/sorting_network.cpp b/src/test/sorting_network.cpp
index 8b2aadee3..a64d3a70f 100644
--- a/src/test/sorting_network.cpp
+++ b/src/test/sorting_network.cpp
@@ -416,7 +416,7 @@ static void test_at_most1() {
     for (unsigned i = 0; i < 5; ++i) {
         in.push_back(m.mk_fresh_const("a",m.mk_bool_sort()));
     }
-    in[4] = in[3];
+    in[4] = in[3].get();
 
     ast_ext2 ext(m);
     psort_nw<ast_ext2> sn(ext);