diff options
Diffstat (limited to 'test/regress/regress0/bv/decision-weight00.smt2')
| -rw-r--r-- | test/regress/regress0/bv/decision-weight00.smt2 | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/test/regress/regress0/bv/decision-weight00.smt2 b/test/regress/regress0/bv/decision-weight00.smt2 deleted file mode 100644 index 1feb32c7f..000000000 --- a/test/regress/regress0/bv/decision-weight00.smt2 +++ /dev/null @@ -1,19 +0,0 @@ -(set-option :produce-models true) -(set-logic QF_BV) -(set-info :source | - Patrice Godefroid, SAGE (systematic dynamic test generation) - For more information: http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf -|) -(set-info :smt-lib-version 2.0) -(set-info :category "industrial") -(set-info :status unknown) -(declare-fun x () (_ BitVec 32)) -(declare-fun y () (_ BitVec 32)) -(declare-fun z () (_ BitVec 4)) -(assert (or - (= x (bvmul x y)) - (and (= x y) - (not (= ((_ extract 2 2) x) ((_ extract 2 2) z)))) - )) -(check-sat) -(exit) |