Merge pull request #12 from funemy/main

add proper bound check for z3 constraints

1 files changed, 16 insertions, 7 deletions

diff --git a/entries/funemy/z3/z3fib.sh b/entries/funemy/z3/z3fib.sh
index 9faa228..07ab418 100755
--- a/entries/funemy/z3/z3fib.sh
+++ b/entries/funemy/z3/z3fib.sh
@@ -1,7 +1,7 @@
 #!/bin/bash
 
-# Instruction:
-#  1. having z3 installed and under you $PATH
+# Instructions:
+#  1. having z3 installed and put under your $PATH
 #  2. making sure z3fib.sh is executable, by `chmod +x z3fib.sh`
 #  3. running as `./z3fib.sh [length of the fib sequence]`
 #  4. having fun :)
@@ -14,6 +14,11 @@ else
     touch fib.smt2
 fi
 
+if [ "$1" -lt "0" ]; then
+  echo "Argument must be larger than 0."
+  exit 1
+fi
+
 for i in $(seq 0 $1);
 do
   echo "(declare-const x$i Int)" >> fib.smt2
@@ -30,12 +35,16 @@ do
 done
 
 echo "    (= x0 0)" >> fib.smt2
-echo "    (= x1 1)" >> fib.smt2
+if [ "$1" -ge "1" ]; then
+  echo "    (= x1 1)" >> fib.smt2
+fi
 
-for i in $(seq 2 $1);
-do
-  echo "    (= x$i (+ x$(($i - 2)) x$(($i - 1))))" >> fib.smt2
-done
+if [ "$1" -ge "2" ]; then
+  for i in $(seq 2 $1);
+  do
+    echo "    (= x$i (+ x$(($i - 2)) x$(($i - 1))))" >> fib.smt2
+  done
+fi
 
 echo "  )" >> fib.smt2
 echo ")" >> fib.smt2