From aef0cca4230ae6a0554d8f0b1a9fbfc36a1f5ef4 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 13 Sep 2023 07:48:29 +0200 Subject: [PATCH] Restoring trailing spaces --- tests/cram.t/run.t | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/tests/cram.t/run.t b/tests/cram.t/run.t index 20ee5c015..3f573aa7f 100644 --- a/tests/cram.t/run.t +++ b/tests/cram.t/run.t @@ -7,7 +7,7 @@ changes slightly, you should be concerned with ensuring the semantic is appropriate here. $ alt-ergo --frontend dolmen --produce-models model555.smt2 --no-forced-flush-in-output 2>/dev/null - + unknown ( (define-fun a1 () (Array Int Int) (store (as @!k1 (Array Int Int)) 0 0)) @@ -18,30 +18,30 @@ appropriate here. Now we will test some semantic triggers. $ alt-ergo --frontend legacy -o smtlib2 semantic_triggers.ae 2>/dev/null - + unknown - + unsat - + unsat $ alt-ergo --frontend dolmen -o smtlib2 semantic_triggers.ae 2>/dev/null - + unknown - + unsat - + unsat And some SMT2 action. $ alt-ergo --frontend dolmen -o smtlib2 --prelude prelude.ae postlude.smt2 2>/dev/null - + unknown - + unsat - + unknown - + unsat Here are some tests to check that we have sane behavior given the insane @@ -75,13 +75,13 @@ And now some cases where it should work (using either `--produce-models` or `Tableaux` with `set-option`): $ echo '(check-sat)(get-model)' | alt-ergo --frontend dolmen --produce-models -i smtlib2 -o smtlib2 2>/dev/null - + unknown ( ) $ echo '(set-option :produce-models true)(check-sat)(get-model)' | alt-ergo --frontend dolmen --sat-solver Tableaux -i smtlib2 -o smtlib2 2>/dev/null - + unknown ( )