diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-01 11:18:00 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-01 11:18:06 -0600 |
| commit | 0615601703a1ac19d485e2b530a748c797b544ed (patch) | |
| tree | 19834cce797501d5586aed222349933c9af16b4a /test | |
| parent | 2ba8bb701ce289ba60afec01b653b0930cc59298 (diff) | |
Simplify fmc model construction, add regression. Improve FMF debug assertions.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/fmf/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/am-bad-model.cvc | 22 |
2 files changed, 24 insertions, 1 deletions
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 8b7202906..370096a1e 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -48,7 +48,8 @@ TESTS = \ tail_rec.smt2 \ jasmin-cdt-crash.smt2 \ loopy_coda.smt2 \ - fmc_unsound_model.smt2 + fmc_unsound_model.smt2 \ + am-bad-model.cvc EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/am-bad-model.cvc b/test/regress/regress0/fmf/am-bad-model.cvc new file mode 100644 index 000000000..e30b5e04a --- /dev/null +++ b/test/regress/regress0/fmf/am-bad-model.cvc @@ -0,0 +1,22 @@ +% EXPECT: sat +OPTION "produce-models"; +OPTION "finite-model-find"; + +f : (BITVECTOR(2),BITVECTOR(2)) ->ARRAY INT OF INT; +f0 : BITVECTOR(2) -> ARRAY INT OF INT; + +td,td1,td2: ARRAY INT OF INT; +ASSERT td1 = td WITH[0]:= 1; +ASSERT td2 = td WITH[0]:= 2; +ASSERT f(0bin01,0bin00)=td1; +ASSERT f(0bin10,0bin00)=td2; +%ASSERT FORALL(i:BITVECTOR(2)) : f0(i)=f(0bin00,i) ; +%Artificial bypass of quantifier for f0 definition +ASSERT f0(0bin00) = f(0bin00,0bin00); +ASSERT f0(0bin01) = f(0bin00,0bin01); +ASSERT f0(0bin10) = f(0bin00,0bin10); +ASSERT f0(0bin11) = f(0bin00,0bin11); +ASSERT FORALL(i:BITVECTOR(2)) : f0(i)=td2 ; + +CHECKSAT; + |