Test -l SimplifyJson

scripts/integration-tests.sh

@@ -52,6 +52,9 @@ for dir in $(ls -d test-*); do
         "simplify")
             SERVER=$BOOSTER_DEV ./runDirectoryTest.sh test-$name $@
             ;;
+        "log-simplify-json")
+            SERVER="${KORE_RPC_BOOSTER} -l SimplifyJson --log-file test-$name/simplify-log.txt" ./runDirectoryTest.sh test-$name $@
+            ;;
         "foundry-bug-report")
             SERVER=$KORE_RPC_BOOSTER ./runDirectoryTest.sh test-$name --time $@
             SERVER=$KORE_RPC_BOOSTER SERVER_OPTS="--interim-simplification 100" ./runDirectoryTest.sh test-$name $@

test/rpc-integration/resources/log-simplify-json.kore

@@ -0,0 +1 @@
+foundry-bug-report.kore

test/rpc-integration/test-log-simplify-json/README.md

@@ -0,0 +1,7 @@
+# Testing logging of equations as JSON
+
+This test sends the request to simplify an initial configuration of a Kontrol proof (based on the `resources/foundry-bug-report.kore` definition).
+The `kore-rpc-booster` server is expected to be started with `-l SimplifyJson --log-file test-log-simplify-json/simplify-log.txt`, which ensures that the equation simplification logs are collected by both Booster and Kore and emitted into a file. The log file is compared to `simplify-log.golden.txt`.
+
+Note: this test may turn out to be flaky, as the logs are sensitive to which equations fail to apply in Booster and why.
+

test/rpc-integration/test-log-simplify-json/test.sh

@@ -0,0 +1,31 @@
+#!/usr/bin/env bash
+
+set -exuo pipefail
+
+# using variables from runDirectoryTest.sh
+
+echo "client=$client"
+echo "dir=$dir"
+echo "arguments=$*"
+
+diff="git diff --no-index"
+# remove "--regenerate" and tweak $diff if it is present
+
+client_args=""
+for arg in $*; do
+    case "$arg" in
+        --regenerate)
+            echo "Re-generating expectation files"
+            diff="tee"
+            ;;
+        *)
+            client_args+=" $arg"
+            ;;
+    esac
+done
+
+# send a simplification request and compare the log files
+echo "Running a request which will produce the simplify-log.txt log file"
+${client} \
+    send $dir/state-002.send ${client_args} > /dev/null
+${diff} $dir/simplify-log.txt.golden $dir/simplify-log.txt