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, 19 insertions, 0 deletions
diff --git a/test/regress/regress0/bv/decision-weight00.smt2 b/test/regress/regress0/bv/decision-weight00.smt2 new file mode 100644 index 000000000..1feb32c7f --- /dev/null +++ b/test/regress/regress0/bv/decision-weight00.smt2 @@ -0,0 +1,19 @@ +(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) |