From 2b23b71fa7fbb52372e8aac6b8f3f6e02cdd506b Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 13 Nov 2011 03:59:36 +0000
Subject: [PATCH] Test case for r1410. Thanks to Stephan Falke.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1413 e59a4935-1847-0410-ae03-e826735625c1
---
 tests/c-api-tests/Makefile          |  7 +++-
 tests/c-api-tests/stp-array-model.c | 58 +++++++++++++++++++++++++++++
 2 files changed, 64 insertions(+), 1 deletion(-)
 create mode 100644 tests/c-api-tests/stp-array-model.c

diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
index e18e2b5..98bf6a8 100644
--- a/tests/c-api-tests/Makefile
+++ b/tests/c-api-tests/Makefile
@@ -14,7 +14,7 @@ else
 endif
 
 
-all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
+all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27
 	rm -rf *.out
 
 0:	
@@ -114,5 +114,10 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26
          ../../lib/libstp.a stp-test3.c ../../lib/libstp.a
 	./a26.out
 
+27:
+	g++ $(CXXFLAGS) -o a27.out \
+         ../../lib/libstp.a stp-array-model.c ../../lib/libstp.a
+	./a27.out
+
 clean:
 	rm -rf *~ *.out *.dSYM
diff --git a/tests/c-api-tests/stp-array-model.c b/tests/c-api-tests/stp-array-model.c
new file mode 100644
index 0000000..e0e2f2c
--- /dev/null
+++ b/tests/c-api-tests/stp-array-model.c
@@ -0,0 +1,58 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include "c_interface.h"
+
+int main() {  
+  VC vc = vc_createValidityChecker();
+
+  Expr a = vc_bvCreateMemoryArray(vc, "a");
+
+  Expr index_1 = vc_bvConstExprFromInt(vc, 32, 1);
+  Expr a_of_1 = vc_readExpr(vc, a, index_1);
+
+  Expr index_2 = vc_bvConstExprFromInt(vc, 32, 2);
+  Expr a_of_2 = vc_readExpr(vc, a, index_2);
+
+  Expr ct_42 = vc_bvConstExprFromInt(vc, 8, 42);
+  Expr a_of_1_eq_42 = vc_eqExpr(vc, a_of_1, ct_42);
+
+  Expr ct_77 = vc_bvConstExprFromInt(vc, 8, 77);
+  Expr a_of_2_eq_77 = vc_eqExpr(vc, a_of_2, ct_77);
+
+  vc_assertFormula(vc, a_of_1_eq_42);
+  vc_assertFormula(vc, a_of_2_eq_77);
+
+  /* query(false) */
+  if (vc_query(vc, vc_falseExpr(vc)) != 0) {
+    printf("Should be invalid...\n");
+    exit(1);
+  }
+
+  if (vc_counterexample_size(vc) == 0) {
+    printf("Counterexample size is 0\n");
+    exit(2);
+  }
+
+  Expr *indices;
+  Expr *values;
+  int size;
+  vc_getCounterExampleArray(vc, a, &indices, &values, &size);
+
+  if (size == 0) {
+    printf("No array entries!\n");
+    exit(3);
+  }
+
+  for (int j = 0; j < size; ++j) {
+    Expr index = vc_getCounterExample(vc, indices[j]);
+    Expr value = vc_getCounterExample(vc, values[j]);
+    unsigned long long i = getBVUnsigned(index);
+    unsigned long long v = getBVUnsigned(value);
+
+    fprintf(stderr, "a[%llu] = %llu\n", i, v);
+  }
+
+  vc_Destroy(vc);
+
+  return 0;
+}
-- 
2.47.3