diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-02 12:22:17 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-02 12:22:17 -0500 |
| commit | e4926117ce53433e59f4b1a86892ea43a01f709d (patch) | |
| tree | 87e12c44b133a4998f38a5988610fe4fdffb82d9 /test | |
| parent | 50edf184492d20f4acb7b8d82f3843f3146f77d5 (diff) | |
Do not handle universal quantification on functions in model-based FMF (#4226)
Fixes #4225, fixes CVC4/cvc4-projects#159, fixes CVC4/cvc4-projects#157, fixes #4289, fixes #4483.
This makes it so that the main model-based instantiation algorithm is not applied to quantified formulas with universally quantified functions.
Identation changed in a FMF function, this was refactored to conform to guidelines, and further cleaned.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/fmf/issue4225-univ-fun.smt2 | 6 |
2 files changed, 7 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 0f1b090d4..2b587c93a 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1315,6 +1315,7 @@ set(regress_1_tests regress1/fmf/issue3626.smt2 regress1/fmf/issue3689.smt2 regress1/fmf/issue4068-si-qf.smt2 + regress1/fmf/issue4225-univ-fun.smt2 regress1/fmf/issue916-fmf-or.smt2 regress1/fmf/jasmin-cdt-crash.smt2 regress1/fmf/ko-bound-set.cvc diff --git a/test/regress/regress1/fmf/issue4225-univ-fun.smt2 b/test/regress/regress1/fmf/issue4225-univ-fun.smt2 new file mode 100644 index 000000000..9946a4567 --- /dev/null +++ b/test/regress/regress1/fmf/issue4225-univ-fun.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --finite-model-find --uf-ho +; EXPECT: unknown +(set-logic ALL) +; this is not handled by fmf +(assert (forall ((a (-> Int Int)) (b Int)) (not (= (a b) 0)))) +(check-sat) |