diff options
Diffstat (limited to 'test/regress')
8 files changed, 9 insertions, 1 deletions
diff --git a/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smt b/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smt index 170239e6f..a14c745a3 100644 --- a/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smt +++ b/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smt @@ -1,3 +1,4 @@ +; COMMAND-LINE: --no-check-proofs (benchmark sc_init_frame_gap.induction.smt :source { The Formal Verification of a Reintegration Protocol. Author: Lee Pike. Website: http://www.cs.indiana.edu/~lepike/pub_pages/emsoft.html. diff --git a/test/regress/regress0/uflra/constants0.smt b/test/regress/regress0/uflra/constants0.smt index b07a6bc4e..87d762e54 100644 --- a/test/regress/regress0/uflra/constants0.smt +++ b/test/regress/regress0/uflra/constants0.smt @@ -1,3 +1,4 @@ +; COMMAND-LINE: --no-check-proofs (benchmark mathsat :logic QF_UFLRA :status unsat @@ -12,4 +13,4 @@ (implies (= (f 3) (f x)) (= (f 5) (f x))) (implies (= (f 3) (f y)) (= (f 5) (f y))) ) -)
\ No newline at end of file +) diff --git a/test/regress/regress0/uflra/pb_real_10_0200_10_22.smt b/test/regress/regress0/uflra/pb_real_10_0200_10_22.smt index 4508d1f85..2c762a941 100644 --- a/test/regress/regress0/uflra/pb_real_10_0200_10_22.smt +++ b/test/regress/regress0/uflra/pb_real_10_0200_10_22.smt @@ -1,3 +1,4 @@ +; COMMAND-LINE: --no-check-proofs (benchmark mathsat :source { MathSat group } :logic QF_UFLRA diff --git a/test/regress/regress0/uflra/pb_real_10_0200_10_26.smt b/test/regress/regress0/uflra/pb_real_10_0200_10_26.smt index d0e9bfed6..84519b5cb 100644 --- a/test/regress/regress0/uflra/pb_real_10_0200_10_26.smt +++ b/test/regress/regress0/uflra/pb_real_10_0200_10_26.smt @@ -1,3 +1,4 @@ +; COMMAND-LINE: --no-check-proofs (benchmark mathsat :source { MathSat group } :logic QF_UFLRA diff --git a/test/regress/regress1/lemmas/pursuit-safety-8.smt b/test/regress/regress1/lemmas/pursuit-safety-8.smt index 5985c500b..efdbc017c 100644 --- a/test/regress/regress1/lemmas/pursuit-safety-8.smt +++ b/test/regress/regress1/lemmas/pursuit-safety-8.smt @@ -1,3 +1,4 @@ +; COMMAND-LINE: --no-check-proofs (benchmark pursuit_safety_8.smt :source { SAL benchmark suite. Created at SRI by Bruno Dutertre, John Rushby, Maria diff --git a/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt b/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt index 506b99b46..ee04fbf34 100644 --- a/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt +++ b/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smt @@ -1,3 +1,4 @@ +; COMMAND-LINE: --no-check-proofs (benchmark tta_startup :source { TTA Startup. Bruno Dutertre (bruno@csl.sri.com) } diff --git a/test/regress/regress2/arith/pursuit-safety-11.smt b/test/regress/regress2/arith/pursuit-safety-11.smt index 1c12e0770..e6365f24c 100644 --- a/test/regress/regress2/arith/pursuit-safety-11.smt +++ b/test/regress/regress2/arith/pursuit-safety-11.smt @@ -1,3 +1,4 @@ +; COMMAND-LINE: --no-check-proofs (benchmark pursuit_safety_11.smt :source { SAL benchmark suite. Created at SRI by Bruno Dutertre, John Rushby, Maria diff --git a/test/regress/regress2/arith/pursuit-safety-12.smt b/test/regress/regress2/arith/pursuit-safety-12.smt index 8f79b3d92..56ebea066 100644 --- a/test/regress/regress2/arith/pursuit-safety-12.smt +++ b/test/regress/regress2/arith/pursuit-safety-12.smt @@ -1,3 +1,4 @@ +; COMMAND-LINE: --no-check-proofs (benchmark pursuit_safety_12.smt :source { SAL benchmark suite. Created at SRI by Bruno Dutertre, John Rushby, Maria |