From 3896f451748a9f5e9fadf94dd65a6d229b8978a9 Mon Sep 17 00:00:00 2001
From: Thomas Tuegel <ttuegel@mailbox.org>
Date: Wed, 16 Jun 2021 10:22:23 -0500
Subject: [PATCH] Clean up golden file for inconsistent-prelude test

---
 test/imp/Makefile                                   | 5 +++--
 test/imp/max-inconsistent-prelude-spec.k.out.golden | 5 -----
 2 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/test/imp/Makefile b/test/imp/Makefile
index bd842aa218..57d1ba76f6 100644
--- a/test/imp/Makefile
+++ b/test/imp/Makefile
@@ -18,8 +18,9 @@ max-inconsistent-prelude-spec.k.out: \
 max-inconsistent-prelude-spec.k.out: max-inconsistent-prelude-spec.k imp.k $(TEST_DEPS)
 	@echo ">>>" $(CURDIR) "kprove" $<
 	rm -f $@
-	$(KPROVE) $(KPROVE_OPTS) $(KPROVE_SPEC) 1> /dev/null 2> $@ || true
-	grep -q "The definitions sent to the solver are inconsistent." $@ || mv $@ $@.fail
+	$(KPROVE) $(KPROVE_OPTS) $(KPROVE_SPEC) 2>&1 1>/dev/null \
+		| grep "inconsistent" > $@ \
+		|| mv $@ $@.fail
 
 max-consistent-prelude-spec.k.out: \
     KPROVE_OPTS += --spec-module MAX-SPEC
diff --git a/test/imp/max-inconsistent-prelude-spec.k.out.golden b/test/imp/max-inconsistent-prelude-spec.k.out.golden
index 8e0bf9d69f..00958d4398 100644
--- a/test/imp/max-inconsistent-prelude-spec.k.out.golden
+++ b/test/imp/max-inconsistent-prelude-spec.k.out.golden
@@ -1,6 +1 @@
-kore-exec: [233424] Error (ErrorException):
     The definitions sent to the solver are inconsistent.
-    CallStack (from HasCallStack):
-      error, called at src/Kore/Step/SMT/Lemma.hs:104:9 in kore-0.40.0.0-CzNxqIvwhPqHJvDm7pwDgz:Kore.Step.SMT.Lemma
-[Error] Critical: Haskell Backend execution failed with code 1 and produced no
-output.