diff options
Diffstat (limited to 'test/regress/regress1/ho/issue4065-no-rep.smt2')
| -rw-r--r-- | test/regress/regress1/ho/issue4065-no-rep.smt2 | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test/regress/regress1/ho/issue4065-no-rep.smt2 b/test/regress/regress1/ho/issue4065-no-rep.smt2 new file mode 100644 index 000000000..841d050a7 --- /dev/null +++ b/test/regress/regress1/ho/issue4065-no-rep.smt2 @@ -0,0 +1,10 @@ +(set-logic AUFBV) +(set-info :status sat) +(set-option :bv-div-zero-const false) +(set-option :fmf-bound-int true) +(set-option :uf-ho true) +(declare-fun _substvar_20_ () Bool) +(declare-sort S4 0) +(assert (forall ((q15 S4) (q16 (_ BitVec 20)) (q17 (_ BitVec 13))) (xor (= (_ bv0 13) (_ bv0 13) q17 (bvsrem (_ bv0 13) (_ bv0 13)) q17) _substvar_20_ true))) +(check-sat) +(exit) |