From eee3ad75a60b1c95663b0bf0bc935a25603a9f57 Mon Sep 17 00:00:00 2001
From: Norbert Manthey <nmanthey@conp-solutions.com>
Date: Wed, 12 Jan 2022 20:44:50 +0100
Subject: [PATCH 1/3] github,workflow: use ubuntu 20.04

Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
---
 .github/workflows/build-and-test-parallel.yml | 2 +-
 .github/workflows/build-and-test.yml          | 2 +-
 .github/workflows/build-werror.yml            | 2 +-
 .github/workflows/check-style.yml             | 2 +-
 .github/workflows/compare-upstream.yml        | 2 +-
 .github/workflows/mini-competition.yml        | 2 +-
 .github/workflows/unit-tests.yml              | 2 +-
 7 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/build-and-test-parallel.yml b/.github/workflows/build-and-test-parallel.yml
index b8233fe1..26d63f1f 100644
--- a/.github/workflows/build-and-test-parallel.yml
+++ b/.github/workflows/build-and-test-parallel.yml
@@ -12,7 +12,7 @@ on:
 jobs:
   Linux:
 
-    runs-on: ubuntu-18.04
+    runs-on: ubuntu-20.04
 
     steps:
     - name: Install Packages
diff --git a/.github/workflows/build-and-test.yml b/.github/workflows/build-and-test.yml
index 28b91e6c..5d16bb08 100644
--- a/.github/workflows/build-and-test.yml
+++ b/.github/workflows/build-and-test.yml
@@ -8,7 +8,7 @@ on:
 jobs:
   CrossARM:
 
-    runs-on: ubuntu-18.04
+    runs-on: ubuntu-20.04
 
     steps:
     - name: Install Packages
diff --git a/.github/workflows/build-werror.yml b/.github/workflows/build-werror.yml
index 6e0a1926..c6c451d9 100644
--- a/.github/workflows/build-werror.yml
+++ b/.github/workflows/build-werror.yml
@@ -8,7 +8,7 @@ on:
 jobs:
   Linux:
 
-    runs-on: ubuntu-18.04
+    runs-on: ubuntu-20.04
 
     steps:
     - name: Install Packages
diff --git a/.github/workflows/check-style.yml b/.github/workflows/check-style.yml
index 1d545fb6..370eba19 100644
--- a/.github/workflows/check-style.yml
+++ b/.github/workflows/check-style.yml
@@ -8,7 +8,7 @@ on:
 jobs:
   Linux:
 
-    runs-on: ubuntu-18.04
+    runs-on: ubuntu-20.04
 
     steps:
     - name: Install Packages
diff --git a/.github/workflows/compare-upstream.yml b/.github/workflows/compare-upstream.yml
index 5abe8dad..5aceca70 100644
--- a/.github/workflows/compare-upstream.yml
+++ b/.github/workflows/compare-upstream.yml
@@ -8,7 +8,7 @@ on:
 jobs:
   Linux:
 
-    runs-on: ubuntu-18.04
+    runs-on: ubuntu-20.04
 
     steps:
     - name: Install Packages
diff --git a/.github/workflows/mini-competition.yml b/.github/workflows/mini-competition.yml
index 9d104b1a..64503ec7 100644
--- a/.github/workflows/mini-competition.yml
+++ b/.github/workflows/mini-competition.yml
@@ -8,7 +8,7 @@ on:
 jobs:
   Linux:
 
-    runs-on: ubuntu-18.04
+    runs-on: ubuntu-20.04
 
     steps:
     - name: Install Packages
diff --git a/.github/workflows/unit-tests.yml b/.github/workflows/unit-tests.yml
index de5d390f..68cd8051 100644
--- a/.github/workflows/unit-tests.yml
+++ b/.github/workflows/unit-tests.yml
@@ -9,7 +9,7 @@ on:
 jobs:
   Linux:
 
-    runs-on: ubuntu-18.04
+    runs-on: ubuntu-20.04
 
     steps:
     - name: Install Packages

From 7bee7e21cda2d025b15aaf9a19193d8f4a52d207 Mon Sep 17 00:00:00 2001
From: Norbert Manthey <nmanthey@conp-solutions.com>
Date: Wed, 12 Jan 2022 23:24:09 +0100
Subject: [PATCH 2/3] ci,fuzzing: use modgen

... because this tool allows to generate more difficult
formulas easily.

While touching scripts, also improve ways how to call related tools.

Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
---
 CHANGELOG                   |  1 +
 tools/checker/check-drat.sh |  6 ++++--
 tools/checker/fuzz-drat.sh  | 26 +++++++++++++++++-------
 tools/checker/fuzzcheck.sh  | 40 +++++++++++++++++++++++--------------
 tools/checker/prepare.sh    | 12 +++++------
 tools/checker/toolCheck.sh  |  5 ++++-
 tools/ci.sh                 |  2 +-
 7 files changed, 59 insertions(+), 33 deletions(-)

diff --git a/CHANGELOG b/CHANGELOG
index 47944af4..378a91c0 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -7,6 +7,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [unreleased]
 
+ * testing: use modgen generator during fuzzing runs
  * fix FPU control to compile on ARM
 
 ## [v3.2.1] - 2021-12-20
diff --git a/tools/checker/check-drat.sh b/tools/checker/check-drat.sh
index 964472d8..32f70f2d 100755
--- a/tools/checker/check-drat.sh
+++ b/tools/checker/check-drat.sh
@@ -11,6 +11,8 @@ shift
 # check for file
 [ -f "$f" ] || exit 2
 
+SCRIPT_DIR="$(cd $(dirname "$0") && pwd)"
+
 # static variables
 p=p.proof
 o=drat-minimize-output.txt
@@ -20,11 +22,11 @@ if [ -n "${FUZZ_SOLVER:-}" ]
 then
 	t=$(readlink -e "${FUZZ_SOLVER:-}")
 fi
-d=$(readlink -e drat-trim)
+d=$(readlink -e "$SCRIPT_DIR"/drat-trim)
 
 # run solver
 STATUS=0
-"$t" "$f" -drup-file=$p $@ || STATUS=$?
+$t "$f" -drup-file="$p" $@ || STATUS=$?
 
 if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ]
 then
diff --git a/tools/checker/fuzz-drat.sh b/tools/checker/fuzz-drat.sh
index 198ec4bd..e5df79e3 100755
--- a/tools/checker/fuzz-drat.sh
+++ b/tools/checker/fuzz-drat.sh
@@ -8,10 +8,14 @@ TIMEOUT=$2
 
 [ -n "$TIMEOUT" ] || exit 2
 
-c=$(readlink -e cnfuzz)
+SCRIPT_DIR="$(cd $(dirname "$0") && pwd)"
+
+c="$SCRIPT_DIR/modgen"
 
 I=0
-f=input.cnf
+f=fuzz_input.cnf
+declare -i found_sat=0
+declare -i found_unsat=0
 
 FAILED=0
 while true
@@ -19,22 +23,30 @@ do
 	I=$((I+1))
 	[ "$LIMIT" -ge "$I" ] || break
 	# echo "[$SECONDS] run $I ..."
-	$c > $f
+	seed="$(echo $(($(date +%s%N)/1000000)))"
+	cls=""
+	while [ -z "$cls" ]; do
+		cls="$(bash -c 'echo $((9000 + $(date +%4N) ))' 2> /dev/null)"
+	done
+	modgen_cli_args="-s $seed -n 3500 -m $cls"
+	$c $modgen_cli_args > $f
 	STATUS=0
-	timeout "$TIMEOUT" ./check-drat.sh $f &> output.log || STATUS=$?
+	timeout "$TIMEOUT" "$SCRIPT_DIR"/check-drat.sh $f &> output.log || STATUS=$?
 	# ignore time outs
 	[ "$STATUS" -ne 124 ] || continue
 
 	# make failures permanent
 	if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ]
 	then
-		echo "[$SECONDS] failed for try $I with status $STATUS and header $(grep "p cnf" input.cnf) seed $(awk '/c seed/ {print $3}' input.cnf)"
-		mv input.cnf input.$I.cnf
+		echo "[$SECONDS] failed for try $I with status $STATUS and header $(grep "p cnf" $f) and generator: $c $modgen_cli_args"
+		mv $f fuzz_input.$I.cnf
 		mv output.log output.$I.log
                 FAILED=$((FAILED+1))
 	fi
+	[ "$STATUS" -eq 10 ] && found_sat=$((found_sat+1))
+	[ "$STATUS" -eq 20 ] && found_unsat=$((found_unsat+1))
 done
 echo "failed $FAILED out of $LIMIT"
-
+echo "($SECONDS s) sat: $found_sat unsat: $found_unsat"
 [ "$FAILED" -eq 0 ] || exit 1
 exit 0
diff --git a/tools/checker/fuzzcheck.sh b/tools/checker/fuzzcheck.sh
index de603c92..c044aa30 100755
--- a/tools/checker/fuzzcheck.sh
+++ b/tools/checker/fuzzcheck.sh
@@ -7,19 +7,19 @@
 prg=$1
 
 # this can be initialized to a max. size of an unreduced buggy formula
-bestcls=5000
+bestcls=50000
 
-cnf=/tmp/runcnfuzz-$$.cnf
-sol=/tmp/runcnfuzz-$$.sol
-err=/tmp/runcnfuzz-$$.err
-out=/tmp/runcnfuzz-$$.out
-log=runcnfuzz-$$.log
+cnf=/dev/shm/uzz-$$.cnf
+sol=/dev/shm/fuzz-$$.sol
+err=/dev/shm/fuzz-$$.err
+out=/dev/shm/fuzz-$$.out
+log=fuzz-$$.log
 rm -f $log $cnf $sol
-echo "[runcnfuzz] running $prg"
-echo "[runcnfuzz] logging $log"
+echo "[fuzz] running $prg"
+echo "[fuzz] logging $log"
 echo "run $1 $2" > $log
-echo "[runcnfuzz] run with pid $$"
-echo "[runcnfuzz] started at $(date)"
+echo "[fuzz] run with pid $$"
+echo "[fuzz] started at $(date)"
 i=0
 
 # set limit for number of instances to be solved
@@ -31,11 +31,19 @@ fi
 test=0
 
 declare -i status=0
+declare -i found_sat=0
+declare -i found_unsat=0
 
 while [ "$test" -lt "$limit" ]
 do
   rm -f $cnf; 
-  ./cnfuzz $CNFUZZOPTIONS > $cnf
+  seed="$(echo $(($(date +%s%N)/1000000)))"
+  cls=""
+  while [ -z "$cls" ]; do
+    cls="$(bash -c 'echo $((6000 + $(date +%4N) ))' 2> /dev/null)"
+  done
+  modgen_cli_args="-s $seed -n 2800 -m $cls"
+  ./modgen $modgen_cli_args > $cnf
   # control whether algorithm should sleep
   seed=`grep 'c seed' $cnf|head -1|awk '{print $NF}'`
   head="`awk '/p cnf /{print $3, $4}' $cnf`"
@@ -68,9 +76,11 @@ do
       continue
       ;;
     10)
+      found_sat=$((found_sat+1))
       continue
       ;;
     20)
+      found_unsat=$((found_unsat+1))
       continue
       ;;
     15)
@@ -82,8 +92,8 @@ do
   status=1
 
   head="`awk '/p cnf /{print $3, $4}' $cnf`"
-  echo "($SECONDS s) [runcnfuzz] bug-$seed $head             with exit code $res"
-  echo "($SECONDS s) To reproduce, run cnfuzz: './cnfuzz $seed > reproduce.cnf' and '$prg reproduce.cnf'"
+  echo "($SECONDS s) [fuzz] bug-$seed $head             with exit code $res"
+  echo "($SECONDS s) To reproduce, run modgen: './modgen $modgen_cli_args > reproduce.cnf' and '$prg reproduce.cnf'"
   echo $seed >> $log
   echo "($SECONDS s) out"
   cat $out
@@ -111,12 +121,12 @@ do
 
   if [ -f "$red" ]; then
     head="`awk '/p cnf /{print $3, $4}' $red`"
-    echo "($SECONDS s) [runcnfuzz] $red $head"
+    echo "($SECONDS s) [fuzz] $red $head"
   fi
   # rm -f $bug
 done
 
-echo "($SECONDS s) "
+echo "($SECONDS s) sat: $found_sat unsat: $found_unsat"
 echo "($SECONDS s) did $test out of $limit tests"
 
 exit $status
diff --git a/tools/checker/prepare.sh b/tools/checker/prepare.sh
index 4daf62ec..0c7a5d9b 100755
--- a/tools/checker/prepare.sh
+++ b/tools/checker/prepare.sh
@@ -1,6 +1,6 @@
 #!/bin/bash
 #
-# This script sets up the checker environment (install drat-trim as well as cnfuzz)
+# This script sets up the checker environment (install drat-trim as well as modgen)
 
 # exits the script immediately if a command exits with a non-zero status
 set -e
@@ -19,12 +19,10 @@ else
 	git clone https://github.com/marijnheule/drat-trim.git drat-trim-src
 fi
 
-# get fuzz tools
-curl http://fmv.jku.at/cnfuzzdd/cnfuzzdd2013.zip > fuzz-suite.zip
-
-# build cnfuzz
-unzip -j -n fuzz-suite.zip cnfuzzdd2013/cnfuzz.c -d .
-gcc -o cnfuzz cnfuzz.c -Wall -O0 -lrt
+# get and build modgen
+git clone --depth=1 git@github.com:conp-solutions/modularityGen.git modgen-src
+make -C modgen-src
+cp modgen-src/modgen .
 
 # build drat-trim
 pushd drat-trim-src
diff --git a/tools/checker/toolCheck.sh b/tools/checker/toolCheck.sh
index 11644ce7..fe980211 100755
--- a/tools/checker/toolCheck.sh
+++ b/tools/checker/toolCheck.sh
@@ -1,3 +1,6 @@
+#!/bin/bash
+
+SCRIPT_DIR="$(cd $(dirname "$0") && pwd)"
 rm -f /tmp/verify_$$.cnf
 
 #echo "run $1 with $2" >> tmp.dat
@@ -18,7 +21,7 @@ fi
 # cat /tmp/verify.cnf
 if [ "$status" -eq "10" ]
 then
-	./verify SAT /tmp/verify_$$.cnf $2 # 2>&1 > /dev/null
+	"$SCRIPT_DIR"/verify SAT /tmp/verify_$$.cnf $2 # 2>&1 > /dev/null
 	vstat=$?
 
 	if [ "$vstat" -eq "1" ]
diff --git a/tools/ci.sh b/tools/ci.sh
index 92e52d59..8d2a9ab2 100755
--- a/tools/ci.sh
+++ b/tools/ci.sh
@@ -37,7 +37,7 @@ test_fuzzing ()
 
     # Perform a basic run, and forward its exit code
     echo "Solve and check $FUZZ_ROUNDS formulas with a 5s timeout"
-    ./fuzz-drat.sh $FUZZ_ROUNDS 5 || STATUS=$?
+    ./fuzz-drat.sh $FUZZ_ROUNDS 15 || STATUS=$?
 
     echo "Fuzz diversity rank configurations ..."
     ./fuzz-check-configurations.sh || STATUS=$?

From 8c2641887dc77ff6f9d5e34e445b5d0ab39be3a8 Mon Sep 17 00:00:00 2001
From: Norbert Manthey <nmanthey@conp-solutions.com>
Date: Fri, 14 Jan 2022 22:55:36 +0100
Subject: [PATCH 3/3] ci,tests: format scripts

Apply formatting.

Signed-off-by: Norbert Manthey <nmanthey@conp-solutions.com>
---
 tools/checker/check-drat.sh |  29 +++---
 tools/checker/fuzz-drat.sh  |  50 +++++------
 tools/checker/fuzzcheck.sh  | 171 +++++++++++++++++-------------------
 tools/checker/prepare.sh    |  17 ++--
 tools/checker/toolCheck.sh  |  87 ++++++++----------
 tools/ci.sh                 |  11 +--
 6 files changed, 169 insertions(+), 196 deletions(-)

diff --git a/tools/checker/check-drat.sh b/tools/checker/check-drat.sh
index 32f70f2d..dae73b6a 100755
--- a/tools/checker/check-drat.sh
+++ b/tools/checker/check-drat.sh
@@ -18,9 +18,8 @@ p=p.proof
 o=drat-minimize-output.txt
 t=$(readlink -e ../../build/release/bin/mergesat)
 # allow to override the solver location via environment variable
-if [ -n "${FUZZ_SOLVER:-}" ]
-then
-	t=$(readlink -e "${FUZZ_SOLVER:-}")
+if [ -n "${FUZZ_SOLVER:-}" ]; then
+    t=$(readlink -e "${FUZZ_SOLVER:-}")
 fi
 d=$(readlink -e "$SCRIPT_DIR"/drat-trim)
 
@@ -28,24 +27,22 @@ d=$(readlink -e "$SCRIPT_DIR"/drat-trim)
 STATUS=0
 $t "$f" -drup-file="$p" $@ || STATUS=$?
 
-if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ]
-then
-	echo "unexpected status code $STATUS"
-	exit $STATUS
+if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ]; then
+    echo "unexpected status code $STATUS"
+    exit $STATUS
 fi
 
 # exclude trivial unsat
 grep "^0$" $f && exit 0
 
 # run the check
-if [ "$STATUS" -ne 20 ]
-then
+if [ "$STATUS" -ne 20 ]; then
     exit $STATUS
 fi
 
 # verify binary proof format
 VERIFY_STATUS=0
-$d $f $p -v -v -n &> $o || exit $VERIFY_STATUS
+$d $f $p -v -v -n &>$o || exit $VERIFY_STATUS
 echo "verify status: $VERIFY_STATUS"
 # for now, don't be too strict
 # grep " does not occur: " $o && exit 3
@@ -54,24 +51,22 @@ exit 20
 # re-run with plain proof format
 "$t" "$f" -drup-file=$p -no-binary-proof $@ || STATUS=$?
 
-if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ]
-then
-	echo "unexpected status code $STATUS"
-	exit $STATUS
+if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ]; then
+    echo "unexpected status code $STATUS"
+    exit $STATUS
 fi
 
 # exclude trivial unsat
 grep "^0$" $f && exit 0
 
 # run the check
-if [ "$STATUS" -ne 20 ]
-then
+if [ "$STATUS" -ne 20 ]; then
     exit $STATUS
 fi
 
 # verify binary proof format
 VERIFY_STATUS=0
-$d $f $p -v -v -n &> $o || exit $VERIFY_STATUS
+$d $f $p -v -v -n &>$o || exit $VERIFY_STATUS
 echo "verify status: $VERIFY_STATUS"
 # for now, don't be too strict
 # grep " does not occur: " $o && exit 3
diff --git a/tools/checker/fuzz-drat.sh b/tools/checker/fuzz-drat.sh
index e5df79e3..abb2c2bb 100755
--- a/tools/checker/fuzz-drat.sh
+++ b/tools/checker/fuzz-drat.sh
@@ -18,33 +18,31 @@ declare -i found_sat=0
 declare -i found_unsat=0
 
 FAILED=0
-while true
-do
-	I=$((I+1))
-	[ "$LIMIT" -ge "$I" ] || break
-	# echo "[$SECONDS] run $I ..."
-	seed="$(echo $(($(date +%s%N)/1000000)))"
-	cls=""
-	while [ -z "$cls" ]; do
-		cls="$(bash -c 'echo $((9000 + $(date +%4N) ))' 2> /dev/null)"
-	done
-	modgen_cli_args="-s $seed -n 3500 -m $cls"
-	$c $modgen_cli_args > $f
-	STATUS=0
-	timeout "$TIMEOUT" "$SCRIPT_DIR"/check-drat.sh $f &> output.log || STATUS=$?
-	# ignore time outs
-	[ "$STATUS" -ne 124 ] || continue
+while true; do
+    I=$((I + 1))
+    [ "$LIMIT" -ge "$I" ] || break
+    # echo "[$SECONDS] run $I ..."
+    seed="$(echo $(($(date +%s%N) / 1000000)))"
+    cls=""
+    while [ -z "$cls" ]; do
+        cls="$(bash -c 'echo $((9000 + $(date +%4N) ))' 2>/dev/null)"
+    done
+    modgen_cli_args="-s $seed -n 3500 -m $cls"
+    $c $modgen_cli_args >$f
+    STATUS=0
+    timeout "$TIMEOUT" "$SCRIPT_DIR"/check-drat.sh $f &>output.log || STATUS=$?
+    # ignore time outs
+    [ "$STATUS" -ne 124 ] || continue
 
-	# make failures permanent
-	if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ]
-	then
-		echo "[$SECONDS] failed for try $I with status $STATUS and header $(grep "p cnf" $f) and generator: $c $modgen_cli_args"
-		mv $f fuzz_input.$I.cnf
-		mv output.log output.$I.log
-                FAILED=$((FAILED+1))
-	fi
-	[ "$STATUS" -eq 10 ] && found_sat=$((found_sat+1))
-	[ "$STATUS" -eq 20 ] && found_unsat=$((found_unsat+1))
+    # make failures permanent
+    if [ "$STATUS" -ne 0 ] && [ "$STATUS" -ne 10 ] && [ "$STATUS" -ne 20 ]; then
+        echo "[$SECONDS] failed for try $I with status $STATUS and header $(grep "p cnf" $f) and generator: $c $modgen_cli_args"
+        mv $f fuzz_input.$I.cnf
+        mv output.log output.$I.log
+        FAILED=$((FAILED + 1))
+    fi
+    [ "$STATUS" -eq 10 ] && found_sat=$((found_sat + 1))
+    [ "$STATUS" -eq 20 ] && found_unsat=$((found_unsat + 1))
 done
 echo "failed $FAILED out of $LIMIT"
 echo "($SECONDS s) sat: $found_sat unsat: $found_unsat"
diff --git a/tools/checker/fuzzcheck.sh b/tools/checker/fuzzcheck.sh
index c044aa30..c2c51408 100755
--- a/tools/checker/fuzzcheck.sh
+++ b/tools/checker/fuzzcheck.sh
@@ -17,16 +17,15 @@ log=fuzz-$$.log
 rm -f $log $cnf $sol
 echo "[fuzz] running $prg"
 echo "[fuzz] logging $log"
-echo "run $1 $2" > $log
+echo "run $1 $2" >$log
 echo "[fuzz] run with pid $$"
 echo "[fuzz] started at $(date)"
 i=0
 
 # set limit for number of instances to be solved
 limit=1
-if [ "x$2" != "x" ]
-then
-  limit=$2
+if [ "x$2" != "x" ]; then
+    limit=$2
 fi
 test=0
 
@@ -34,96 +33,90 @@ declare -i status=0
 declare -i found_sat=0
 declare -i found_unsat=0
 
-while [ "$test" -lt "$limit" ]
-do
-  rm -f $cnf; 
-  seed="$(echo $(($(date +%s%N)/1000000)))"
-  cls=""
-  while [ -z "$cls" ]; do
-    cls="$(bash -c 'echo $((6000 + $(date +%4N) ))' 2> /dev/null)"
-  done
-  modgen_cli_args="-s $seed -n 2800 -m $cls"
-  ./modgen $modgen_cli_args > $cnf
-  # control whether algorithm should sleep
-  seed=`grep 'c seed' $cnf|head -1|awk '{print $NF}'`
-  head="`awk '/p cnf /{print $3, $4}' $cnf`"
-  [ -n "${VERBOSE_FUZZING:-}" ] && printf "%d %16d          %6d    %6d               \r" "$i" "$seed" $head
-  i=`expr $i + 1`
-  rm -f $sol
-
-  # set limit for number of instances to be solved
-  if [ "x$2" != "x" ]
-  then
-    test=$(($test+1))
-  fi
-
-  thiscls=`awk '/p cnf /{print $4}' $cnf`
-  if [ $bestcls -ne "-1" ]
-  then
-    if [ $bestcls -le $thiscls ]
-    then
-      continue
+while [ "$test" -lt "$limit" ]; do
+    rm -f $cnf
+    seed="$(echo $(($(date +%s%N) / 1000000)))"
+    cls=""
+    while [ -z "$cls" ]; do
+        cls="$(bash -c 'echo $((6000 + $(date +%4N) ))' 2>/dev/null)"
+    done
+    modgen_cli_args="-s $seed -n 2800 -m $cls"
+    ./modgen $modgen_cli_args >$cnf
+    # control whether algorithm should sleep
+    seed=$(grep 'c seed' $cnf | head -1 | awk '{print $NF}')
+    head="$(awk '/p cnf /{print $3, $4}' $cnf)"
+    [ -n "${VERBOSE_FUZZING:-}" ] && printf "%d %16d          %6d    %6d               \r" "$i" "$seed" $head
+    i=$(expr $i + 1)
+    rm -f $sol
+
+    # set limit for number of instances to be solved
+    if [ "x$2" != "x" ]; then
+        test=$(($test + 1))
+    fi
+
+    thiscls=$(awk '/p cnf /{print $4}' $cnf)
+    if [ "$bestcls" -ne "-1" ]; then
+        if [ "$bestcls" -le "$thiscls" ]; then
+            continue
+        fi
     fi
-  fi
 
-  ./toolCheck.sh $prg $cnf > $out 2> $err
-  res=$?
-#  echo "result $res"
-  case $res in
+    ./toolCheck.sh $prg $cnf >$out 2>$err
+    res=$?
+    #  echo "result $res"
+    case $res in
     124)
-      echo "($SECONDS s) timeout with $seed" > $log
-      mv $cnf timeout-$seed.cnf
-      continue
-      ;;
+        echo "($SECONDS s) timeout with $seed" >$log
+        mv $cnf timeout-$seed.cnf
+        continue
+        ;;
     10)
-      found_sat=$((found_sat+1))
-      continue
-      ;;
+        found_sat=$((found_sat + 1))
+        continue
+        ;;
     20)
-      found_unsat=$((found_unsat+1))
-      continue
-      ;;
-    15)
-    ;;
-    25)
-    ;;
-  esac
-
-  status=1
-
-  head="`awk '/p cnf /{print $3, $4}' $cnf`"
-  echo "($SECONDS s) [fuzz] bug-$seed $head             with exit code $res"
-  echo "($SECONDS s) To reproduce, run modgen: './modgen $modgen_cli_args > reproduce.cnf' and '$prg reproduce.cnf'"
-  echo $seed >> $log
-  echo "($SECONDS s) out"
-  cat $out
-  echo "($SECONDS s) err"
-  cat $err
-  
-  #
-  # consider only bugs that are smaller then the ones we found already
-  #
-  if [ $bestcls -eq "-1" ]
-  then
-    bestcls=$thiscls
-    echo "($SECONDS s) init bestcls with $bestcls"
-  elif [ $bestcls -le $thiscls ]
-  then
-    echo "($SECONDS s) reject new bug with $thiscls clauses"
-    continue
-  fi
-  
-  bestcls=$thiscls # store better clause count!
-  echo "($SECONDS s) set bestcls to $bestcls"
-  red=red-$seed.cnf
-  bug=bug-$seed.cnf
-  mv $cnf $bug
-
-  if [ -f "$red" ]; then
-    head="`awk '/p cnf /{print $3, $4}' $red`"
-    echo "($SECONDS s) [fuzz] $red $head"
-  fi
-  # rm -f $bug
+        found_unsat=$((found_unsat + 1))
+        continue
+        ;;
+    15) ;;
+
+    25) ;;
+
+    esac
+
+    status=1
+
+    head="$(awk '/p cnf /{print $3, $4}' $cnf)"
+    echo "($SECONDS s) [fuzz] bug-$seed $head             with exit code $res"
+    echo "($SECONDS s) To reproduce, run modgen: './modgen $modgen_cli_args > reproduce.cnf' and '$prg reproduce.cnf'"
+    echo $seed >>$log
+    echo "($SECONDS s) out"
+    cat $out
+    echo "($SECONDS s) err"
+    cat $err
+
+    #
+    # consider only bugs that are smaller then the ones we found already
+    #
+    if [ "$bestcls" -eq "-1" ]; then
+        bestcls=$thiscls
+        echo "($SECONDS s) init bestcls with $bestcls"
+    elif [ "$bestcls" -le $thiscls ]; then
+        echo "($SECONDS s) reject new bug with $thiscls clauses"
+        continue
+    fi
+
+    bestcls="$thiscls" # store better clause count!
+    echo "($SECONDS s) set bestcls to $bestcls"
+    red=red-$seed.cnf
+    bug=bug-$seed.cnf
+    mv $cnf $bug
+
+    if [ -f "$red" ]; then
+        head="$(awk '/p cnf /{print $3, $4}' $red)"
+        echo "($SECONDS s) [fuzz] $red $head"
+    fi
+    # rm -f $bug
 done
 
 echo "($SECONDS s) sat: $found_sat unsat: $found_unsat"
diff --git a/tools/checker/prepare.sh b/tools/checker/prepare.sh
index 0c7a5d9b..b19177d8 100755
--- a/tools/checker/prepare.sh
+++ b/tools/checker/prepare.sh
@@ -6,21 +6,20 @@
 set -e
 
 # directory of this script (in repo/scripts)
-script_dir=$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )
+script_dir=$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)
 
 # get drat-trim
-if [ -d drat-trim-src ]
-then
-	pushd drat-trim-src
-	git fetch origin
-	git checkout origin/master
-	popd
+if [ -d drat-trim-src ]; then
+    pushd drat-trim-src
+    git fetch origin
+    git checkout origin/master
+    popd
 else
-	git clone https://github.com/marijnheule/drat-trim.git drat-trim-src
+    git clone https://github.com/marijnheule/drat-trim.git drat-trim-src
 fi
 
 # get and build modgen
-git clone --depth=1 git@github.com:conp-solutions/modularityGen.git modgen-src
+git clone --depth=1 https://github.com/conp-solutions/modularityGen.git modgen-src
 make -C modgen-src
 cp modgen-src/modgen .
 
diff --git a/tools/checker/toolCheck.sh b/tools/checker/toolCheck.sh
index fe980211..9e373014 100755
--- a/tools/checker/toolCheck.sh
+++ b/tools/checker/toolCheck.sh
@@ -5,71 +5,62 @@ rm -f /tmp/verify_$$.cnf
 
 #echo "run $1 with $2" >> tmp.dat
 
-timeout 10 $1 $2 > /tmp/verify_$$.cnf 2> /tmp/verify2_$$.cnf;
+timeout 10 $1 $2 >/tmp/verify_$$.cnf 2>/tmp/verify2_$$.cnf
 status=$?
 # sleep 0.01
 
 #echo "finish with state= $status" >> tmp.dat
 
-if [ "$status" -eq "124" ]
-then
-	# we got a timeout here!
-	rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf
-	exit 124
+if [ "$status" -eq "124" ]; then
+    # we got a timeout here!
+    rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf
+    exit 124
 fi
 
 # cat /tmp/verify.cnf
-if [ "$status" -eq "10" ]
-then
-	"$SCRIPT_DIR"/verify SAT /tmp/verify_$$.cnf $2 # 2>&1 > /dev/null
-	vstat=$?
+if [ "$status" -eq "10" ]; then
+    "$SCRIPT_DIR"/verify SAT /tmp/verify_$$.cnf $2 # 2>&1 > /dev/null
+    vstat="$?"
 
-	if [ "$vstat" -eq "1" ]
-	then
-		rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf
-		exit 10
-	else
-		echo "solver out:"
-		cat /tmp/verify_$$.cnf
-		echo "solver err:"
-		cat /tmp/verify2_$$.cnf
-		rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf
-		exit 15
-	fi
+    if [ "$vstat" -eq "1" ]; then
+        rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf
+        exit 10
+    else
+        echo "solver out:"
+        cat /tmp/verify_$$.cnf
+        echo "solver err:"
+        cat /tmp/verify2_$$.cnf
+        rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf
+        exit 15
+    fi
 else
-	# if the instance is unsatisfiable or another error occurred, report it
-#	echo "exit with $status" >> tmp.dat
-
+    # if the instance is unsatisfiable or another error occurred, report it
+    #	echo "exit with $status" >> tmp.dat
 
-     if [ "$status" -ne "20" ]
-     then
-         echo "solver output:"
-         cat /tmp/verify_$$.cnf /tmp/verify2_$$.cnf
-	rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf
-	exit $status
-     fi
+    if [ "$status" -ne "20" ]; then
+        echo "solver output:"
+        cat /tmp/verify_$$.cnf /tmp/verify2_$$.cnf
+        rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf
+        exit $status
+    fi
 
+    timeout 30 picosat $2 2>/dev/null 1>/dev/null
+    lstat=$?
 
-     timeout 30 picosat $2 2> /dev/null 1> /dev/null
-     lstat=$?
-
-     if [ "$status" -eq "124" ]
-     then
+    if [ "$status" -eq "124" ]; then
         # we got a timeout here!
-	mkdir -p picosatTimeout # collect instances where lingeling performs badly
+        mkdir -p picosatTimeout # collect instances where lingeling performs badly
         mv $2 picosatTimeout
-	rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf
+        rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf
         exit 124
-     fi
+    fi
 
-     if [ $lstat -ne "20" ]
-     then
-       echo "solver output:"
-       cat /tmp/verify_$$.cnf /tmp/verify2_$$.cnf
-       rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf
-       exit 25
-     fi
+    if [ $lstat -ne "20" ]; then
+        echo "solver output:"
+        cat /tmp/verify_$$.cnf /tmp/verify2_$$.cnf
+        rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf
+        exit 25
+    fi
     rm -f /tmp/verify_$$.cnf /tmp/verify2_$$.cnf
     exit 20
 fi
-
diff --git a/tools/ci.sh b/tools/ci.sh
index 8d2a9ab2..d7272954 100755
--- a/tools/ci.sh
+++ b/tools/ci.sh
@@ -27,13 +27,12 @@ CHECKERDIR=$(readlink -e tools/checker)
 
 STATUS=0
 
-test_fuzzing ()
-{
+test_fuzzing() {
     # Enter checker repository
     pushd tools/checker
 
     # Checkout and build required tools
-    ./prepare.sh
+    ./prepare.sh || return 1
 
     # Perform a basic run, and forward its exit code
     echo "Solve and check $FUZZ_ROUNDS formulas with a 5s timeout"
@@ -51,8 +50,7 @@ if [ $TESTFUZZ -eq 1 ]; then
     echo "[$SECONDS s] end fuzzing"
 fi
 
-test_diversify ()
-{
+test_diversify() {
     # Enter checker repository
     pushd tools/checker
 
@@ -83,8 +81,7 @@ STATIC_LIB=$(readlink -e build/release/lib/libmergesat.a)
 MERGEZIP=$(ls MergeSAT*.zip | sort -V | tail -n 1)
 MERGEZIP=$(readlink -e $MERGEZIP)
 
-test_starexec ()
-{
+test_starexec() {
 
     [ $CLEANUP -eq 0 ] || trap 'rm -rf $TMPD' EXIT
     TMPD=$(mktemp -d)