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 f5a7dd7d89..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: [10415077] Error (ErrorException): The definitions sent to the solver are inconsistent. - CallStack (from HasCallStack): - error, called at src/Kore/Step/SMT/Lemma.hs:106:9 in kore-0.45.0.0-wxhTBooqYV3YocNuIDw2u:Kore.Step.SMT.Lemma -[Error] Critical: Haskell Backend execution failed with code 1 and produced no -output.