diff options
Diffstat (limited to 'test/regress/regress0/aufbv/fuzz05.delta01.smt')
| -rw-r--r-- | test/regress/regress0/aufbv/fuzz05.delta01.smt | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test/regress/regress0/aufbv/fuzz05.delta01.smt b/test/regress/regress0/aufbv/fuzz05.delta01.smt new file mode 100644 index 000000000..b2dfdceff --- /dev/null +++ b/test/regress/regress0/aufbv/fuzz05.delta01.smt @@ -0,0 +1,14 @@ +(benchmark fuzzsmt +:logic QF_AUFBV +:extrafuns ((a2 Array[12:9])) +:status sast +:formula +(let (?n1 bv0[13]) +(let (?n2 (bvsdiv ?n1 ?n1)) +(let (?n3 bv0[12]) +(let (?n4 (select a2 ?n3)) +(let (?n5 (sign_extend[4] ?n4)) +(let (?n6 (bvmul ?n2 ?n5)) +(flet ($n7 (bvsge ?n1 ?n6)) +$n7 +)))))))) |