diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-05 12:02:28 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-05 12:11:02 +0200 |
| commit | c38245e4f041252df011a024abe834ae7ec0ec0a (patch) | |
| tree | 0452b7a998312393a2556c6cdf695af17efb91d4 /test/regress/regress0 | |
| parent | d3c365a60c88e33a7d73f81484db2cff5ef69bbb (diff) | |
Fix bugs related to fmf with incremental. Reinitialize sorts on user pop, bug fix enumeration for uninitialized sorts, do not decide combined cardinality constraints that have not been allocated in user context. Fixes bug 654.
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/push-pop/Makefile.am | 3 | ||||
| -rwxr-xr-x | test/regress/regress0/push-pop/bug654-dd.smt2 | 27 |
2 files changed, 29 insertions, 1 deletions
diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index 59531ce8a..bcd8da228 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -39,7 +39,8 @@ BUG_TESTS = \ arith_lra_02.smt2 \ quant-fun-proc.smt2 \ quant-fun-proc-unmacro.smt2 \ - quant-fun-proc-unfd.smt2 + quant-fun-proc-unfd.smt2 \ + bug654-dd.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/push-pop/bug654-dd.smt2 b/test/regress/regress0/push-pop/bug654-dd.smt2 new file mode 100755 index 000000000..01c81cdc8 --- /dev/null +++ b/test/regress/regress0/push-pop/bug654-dd.smt2 @@ -0,0 +1,27 @@ +; COMMAND-LINE: --incremental --fmf-fun --strings-exp +(set-logic ALL_SUPPORTED) +(declare-datatypes () ( +(List_T_C (List_T_C$CNil_T_CustomerType) (ListTC (ListTC$head T_CustomerType) (ListTC$tail List_T_C))) +(T_CustomerType (T_CustomerType$C_T_CustomerType (T_CustomerType$C_T_CustomerType$a_CompanyName Int) (T_CustomerType$C_T_CustomerType$a_ContactName Int) (ID Int))) +)) +(declare-fun f (List_T_C) Bool) +(declare-fun tail_uf_1 (List_T_C) List_T_C) +(declare-fun head_uf_2 (List_T_C) T_CustomerType) +(declare-sort U 0) +(declare-fun a (U) List_T_C) +(declare-fun z (U) U) +(assert +(forall ((?i U)) +(= (f (a ?i)) (not (is-ListTC (a ?i))) +))) +(assert +(forall ((?i U)) +(= (a (z ?i)) (tail_uf_1 (a ?i)))) ) +; EXPECT: sat +(push 1) +(check-sat) +(pop 1) +; EXPECT: sat +(push 1) +(check-sat) +(pop 1)
\ No newline at end of file |