From 7da550999d154831210fb381470dba6a8ceb3ced Mon Sep 17 00:00:00 2001 From: Steven de Oliveira Date: Tue, 26 Sep 2023 17:08:08 +0200 Subject: [PATCH] Make test more interesting --- tests/everything/testfile-smt-instr-get-info.dolmen.expected | 4 ++-- tests/everything/testfile-smt-instr-get-info.dolmen.smt2 | 3 ++- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/tests/everything/testfile-smt-instr-get-info.dolmen.expected b/tests/everything/testfile-smt-instr-get-info.dolmen.expected index b0fd09f5ab..5aa61ed6b2 100644 --- a/tests/everything/testfile-smt-instr-get-info.dolmen.expected +++ b/tests/everything/testfile-smt-instr-get-info.dolmen.expected @@ -1,11 +1,11 @@ (error "Invalid (get-info :reason-unknown)") -unsat +unknown (:all-statistics unsupported) (:assertion-stack-levels unsupported) (:authors "Alt-Ergo developers") (:error-behavior immediate-exit) (:name "Alt-Ergo") -(error "Invalid (get-info :reason-unknown)") +(:reason-unknown incomplete) (:version dev) (error "unknown option ':foo'") diff --git a/tests/everything/testfile-smt-instr-get-info.dolmen.smt2 b/tests/everything/testfile-smt-instr-get-info.dolmen.smt2 index 15b011cb05..4fd233ce50 100644 --- a/tests/everything/testfile-smt-instr-get-info.dolmen.smt2 +++ b/tests/everything/testfile-smt-instr-get-info.dolmen.smt2 @@ -2,7 +2,8 @@ (declare-const x Int) (declare-const y Int) -(assert (= (* x x) 3)) + +(assert (= (* x x) 4)) (get-info :reason-unknown) (check-sat)