diff options
Diffstat (limited to 'test/regress/regress2')
| -rw-r--r-- | test/regress/regress2/bv_to_int_5095_2.smt2 | 4 | ||||
| -rw-r--r-- | test/regress/regress2/quantifiers/net-policy-no-time.smt2 | 2 |
2 files changed, 4 insertions, 2 deletions
diff --git a/test/regress/regress2/bv_to_int_5095_2.smt2 b/test/regress/regress2/bv_to_int_5095_2.smt2 index 54dfa0946..234e82229 100644 --- a/test/regress/regress2/bv_to_int_5095_2.smt2 +++ b/test/regress/regress2/bv_to_int_5095_2.smt2 @@ -1,6 +1,6 @@ ; EXPECT: sat -; COMMAND --solve-bv-as-int=sum +; COMMAND-LINE: --solve-bv-as-int=sum -q (set-logic BV) (declare-const bv_42-0 (_ BitVec 42)) (assert (exists ((q28 (_ BitVec 42))) (distinct (bvudiv bv_42-0 bv_42-0) q28))) -(check-sat)
\ No newline at end of file +(check-sat) diff --git a/test/regress/regress2/quantifiers/net-policy-no-time.smt2 b/test/regress/regress2/quantifiers/net-policy-no-time.smt2 index 938aa01ea..b688d3fcf 100644 --- a/test/regress/regress2/quantifiers/net-policy-no-time.smt2 +++ b/test/regress/regress2/quantifiers/net-policy-no-time.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: -q +; EXPECT: sat (set-logic UFDTLIRA) (set-option :fmf-bound true) (set-option :finite-model-find true) |