From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 26 Sep 2012 16:42:40 +0000 (+0000)
Subject: bug #398 test (bug was resolved last night), and a script to download all bug attachm... 
X-Git-Tag: cvc5-1.0.0~7783
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f6fcb28606d8eca239c3a71e7f42a2bbbf0a8995;p=cvc5.git

bug #398 test (bug was resolved last night), and a script to download all bug attachments from bugzilla and put them in the tree
---

diff --git a/contrib/get-bug-attachments b/contrib/get-bug-attachments
new file mode 100755
index 000000000..16af3c67f
--- /dev/null
+++ b/contrib/get-bug-attachments
@@ -0,0 +1,75 @@
+#!/bin/bash
+#
+# get-bug-attachments
+# Morgan Deters <mdeters@cs.nyu.edu>
+# Wed, 26 Sep 2012 09:40:10 -0400
+#
+
+if [ $# -lt 1 ]; then
+  echo "usage: `basename $0` bugids.." >&2
+  exit 1
+fi
+
+while [ $# -gt 0 ]; do
+
+bugid="$1"
+shift
+
+function webcat {
+  if which wget &>/dev/null; then
+    wget -O - "$1"
+  elif which curl &>/dev/null; then
+    curl "$1"
+  else
+    echo "Please install wget or curl." >&2;
+    exit 1
+  fi
+}
+
+function webget {
+  if which wget &>/dev/null; then
+    tmpfile="$(mktemp)"
+    filename="$(wget -qS -O "$tmpfile" "$1" 2>&1 | grep 'Content-disposition: attachment' | sed 's,.*filename="\(.*\)".*,\1,')"
+    ext="$(echo "$filename" | sed 's,.*\.\(.*\),\1,')"
+    if [ -e "$2.$ext" ] && ! diff -q "$tmpfile" "$2.$ext" &>/dev/null; then
+      c=a
+      while [ -e "$2$c.$ext" ] && ! diff -q "$tmpfile" "$2$c.$ext" &>/dev/null; do
+        c=$(echo $c | tr a-y b-z)
+      done
+      mkdir -p "$(dirname "$2")"
+      mv "$tmpfile" "$2$c.$ext"
+      echo "$2$c.$ext"
+    else
+      mkdir -p "$(dirname "$2")"
+      mv "$tmpfile" "$2.$ext"
+      echo "$2.$ext"
+    fi
+  elif which curl &>/dev/null; then
+    mkdir -p "$(dirname "$2")"
+    curl "$1" >"$2"
+  else
+    echo "Please install wget or curl." >&2;
+    exit 1
+  fi
+}
+
+count=0
+for attachment in $(\
+  webcat "http://church.cims.nyu.edu/bugs/show_bug.cgi?id=$bugid" 2>/dev/null \
+  | grep ' href="attachment.cgi?id=[0-9][0-9]*' \
+  | sed 's,.* href="attachment.cgi?id=\([0-9][0-9]*\).*,\1,' \
+  | sort -nu); do
+
+  let count++
+  echo -n "Downloading attachment $attachment..."
+  webget "http://church.cims.nyu.edu/bugs/attachment.cgi?id=$attachment" "test/regress/regress0/bug$bugid"
+
+done
+
+if [ $count -eq 0 ]; then
+  echo "There are no bug testcase attachments for bug #$bugid."
+else
+  echo "Downloaded $count bug testcases for bug #$bugid."
+fi
+
+done
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 50527e51a..ed12c447e 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -128,7 +128,8 @@ BUG_TESTS = \
 	bug339.smt2 \
 	bug365.smt2 \
 	bug382.smt2 \
-	bug383.smt2
+	bug383.smt2 \
+	bug398.smt2
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bug398.smt2 b/test/regress/regress0/bug398.smt2
new file mode 100644
index 000000000..0423d11a4
--- /dev/null
+++ b/test/regress/regress0/bug398.smt2
@@ -0,0 +1,3 @@
+% EXIT: 0
+(set-logic QF_LRA)
+(define-fun x () Real (+ 4 1))