From 5259187264dccfee14e8d74f0ac2c24311da6669 Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Tue, 28 Nov 2023 14:10:18 +0100 Subject: [PATCH] Update tests --- tests/cram.t/run.t | 6 +++--- tests/smtlib/testfile-steps-bound1.dolmen.err.expected | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t index 68fc46aa09..bf837bf48a 100644 --- a/tests/cram.t/run.t +++ b/tests/cram.t/run.t @@ -42,16 +42,16 @@ combinations of produce-models et al. First, if (get-model) is called outside the SAT mode, we should fail. $ echo '(get-model)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error 2> /dev/null - (error "Invalid action during mode Start: Command get-model") + (error "Invalid action during Start mode: Command get-model") $ echo '(set-logic ALL)(get-model)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error 2> /dev/null - (error "Invalid action during mode Assert: Command get-model") + (error "Invalid action during Assert mode: Command get-model") $ echo '(set-logic ALL)(assert false)(check-sat)(get-model)' | alt-ergo -i smtlib2 -o smtlib2 --continue-on-error 2> /dev/null unsat - (error "Invalid action during mode Unsat: Command get-model") + (error "Invalid action during Unsat mode: Command get-model") Then, if model generation is not enabled, we should error out when a `(get-model)` statement is issued: diff --git a/tests/smtlib/testfile-steps-bound1.dolmen.err.expected b/tests/smtlib/testfile-steps-bound1.dolmen.err.expected index be8487e618..4536febdd6 100644 --- a/tests/smtlib/testfile-steps-bound1.dolmen.err.expected +++ b/tests/smtlib/testfile-steps-bound1.dolmen.err.expected @@ -1 +1 @@ -(error "Invalid action during mode Assert: Set option steps_bound") +(error "Invalid action during Assert mode: Set option steps_bound")