From e66924cb0f425ca70969058532340e68c9c17a54 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 16 Nov 2010 19:18:19 +0000 Subject: SmtEngine now fails with a ModalException if --incremental is not enabled but a push/pop or multiple query is attempted (previously it could give incorrect answers) Also, fix some multi-query and push-pop tests that had wrong answers, and support a new "% COMMAND-LINE: " gesture in regression tests so that a test can pass additional, specific command line flags it wants to run with (here, --incremental). Also fix mkbuilddir script for when it's called from contrib/switch-config. --- test/regress/regress0/push-pop/test.00.cvc | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'test/regress/regress0/push-pop/test.00.cvc') diff --git a/test/regress/regress0/push-pop/test.00.cvc b/test/regress/regress0/push-pop/test.00.cvc index 38d720227..f56abb386 100644 --- a/test/regress/regress0/push-pop/test.00.cvc +++ b/test/regress/regress0/push-pop/test.00.cvc @@ -1,3 +1,4 @@ +% COMMAND-LINE: --incremental x: BOOLEAN; PUSH; @@ -6,6 +7,6 @@ ASSERT x; CHECKSAT; POP; ASSERT (NOT x); -% EXPECT: unsat +% EXPECT: sat CHECKSAT; -% EXIT: 20 +% EXIT: 10 -- cgit v1.2.3