diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-12-22 12:03:10 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-12-22 12:03:10 +0100 |
| commit | bd6a13bbb46c272561c01b7783f62ff7be091c2c (patch) | |
| tree | 0fb8e93664b68b961878a9a208423aaa5e85656a /test | |
| parent | 5f207ba01302c3245e169bfbe2ed91ad0cd659cd (diff) | |
Bug fix for cbqi, do not use model values for terms involving non-enumerable sorts.
Diffstat (limited to 'test')
| -rwxr-xr-x | test/regress/regress0/fmf/forall_unit_data.smt2 | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/test/regress/regress0/fmf/forall_unit_data.smt2 b/test/regress/regress0/fmf/forall_unit_data.smt2 new file mode 100755 index 000000000..7e0897d14 --- /dev/null +++ b/test/regress/regress0/fmf/forall_unit_data.smt2 @@ -0,0 +1,13 @@ +; cvc4 --lang smt
+
+; This problem returns "unsat", but it is in fact "sat", by interpreting "a" with a domain of
+; cardinality 1. The issue arises irrespective of the "--finite-model-find" option.
+
+(set-option :produce-models true)
+(set-option :interactive-mode true)
+(set-logic ALL_SUPPORTED)
+(declare-sort a 0)
+(declare-datatypes () ((w (Wrap (unw a)))))
+(declare-fun x () w)
+(assert (forall ((y w)) (= x y)))
+(check-sat)
|