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 | |
| parent | ed2aa5d552a86fe3e4798ef03c995f54abe20cb9 (diff) | |
Do not assign higher-order representative if function does not exist (#4073)
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/ho/issue4065-no-rep.smt2 | 10 |
2 files changed, 11 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index fd4f2aef0..be96ca70d 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1300,6 +1300,7 @@ set(regress_1_tests regress1/gensys_brn001.smt2 regress1/ho/fta0328.lfho.p regress1/ho/issue3136-fconst-bool-bool.smt2 + regress1/ho/issue4065-no-rep.smt2 regress1/ho/nested_lambdas-AGT034^2.smt2 regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 regress1/ho/NUM638^1.smt2 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) |