diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-20 13:18:11 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-03-20 13:18:11 -0500 |
| commit | aa44c35f035f1cab03de0c5fe7c0f16b20f44696 (patch) | |
| tree | c50d4bbb5cfeee385b2f5d1bf8e5b9281def3859 /test/regress/regress1/ho | |
| parent | ed2aa5d552a86fe3e4798ef03c995f54abe20cb9 (diff) | |
Do not assign higher-order representative if function does not exist (#4073)
Diffstat (limited to 'test/regress/regress1/ho')
| -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) |