diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-05 15:32:48 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-05 15:32:48 +0100 |
| commit | 36a5437abbddd484b8bdb18c024cc7573240054f (patch) | |
| tree | 587994c441c49995624029c9094c5caeed9cf7d1 /test | |
| parent | a84864da338f74958c6754696d98cd6355e798a8 (diff) | |
More work on datatypes theory combination: fix bug in care graph, do not assign values for EQC of datatype type that contain only terms belonging to other theories, do not treat APPLY_UF as congruence operator, communicate equalities involving terms of external kind. Minor fixes for fun_def_process. Other minor changes.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 1 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 | 31 |
2 files changed, 32 insertions, 0 deletions
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index e3bfd39b8..cb58ea007 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -40,6 +40,7 @@ EXTRA_DIST = $(TESTS) # disabled for now : # bug0909.smt2 +# lst-no-self-rev-exp.smt2 #if CVC4_BUILD_PROFILE_COMPETITION #else diff --git a/test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 b/test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 new file mode 100644 index 000000000..e86d8c60e --- /dev/null +++ b/test/regress/regress0/fmf/lst-no-self-rev-exp.smt2 @@ -0,0 +1,31 @@ +; COMMAND-LINE: --finite-model-find --uf-ss-fair +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(declare-datatypes () ((Nat (succ (pred Nat)) (zero)) (Lst (cons (hd Nat) (tl Lst)) (nil)))) + +(declare-fun app (Lst Lst) Lst) +(declare-fun rev (Lst) Lst) + +(declare-sort I_app 0) +(declare-sort I_rev 0) + +(declare-fun app_0_3 (I_app) Lst) +(declare-fun app_1_4 (I_app) Lst) +(declare-fun rev_0_5 (I_rev) Lst) + +(declare-fun xs () Lst) + +(assert (and + +(forall ((?i I_app)) (= (app (app_0_3 ?i) (app_1_4 ?i)) (ite (is-cons (app_0_3 ?i)) (cons (hd (app_0_3 ?i)) (app (tl (app_0_3 ?i)) (app_1_4 ?i))) (app_1_4 ?i))) ) + +(forall ((?i I_rev)) (= (rev (rev_0_5 ?i)) (ite (is-cons (rev_0_5 ?i)) (app (rev (tl (rev_0_5 ?i))) (cons (hd (rev_0_5 ?i)) nil)) nil)) ) + +(forall ((?i I_rev)) (or (not (is-cons (rev_0_5 ?i))) (and (not (forall ((?z I_app)) (not (and (= (app_0_3 ?z) (rev (tl (rev_0_5 ?i)))) (= (app_1_4 ?z) (cons (hd (rev_0_5 ?i)) nil)))) )) (not (forall ((?z I_rev)) (not (= (rev_0_5 ?z) (tl (rev_0_5 ?i)) )) )))) ) + +(not (or (= xs (rev xs)) (forall ((?z I_rev)) (not (= (rev_0_5 ?z) xs)) ))) + +)) + +(check-sat) + |