diff options
Diffstat (limited to 'test/regress/regress1/fmf/am-bad-model.cvc')
-rw-r--r-- | test/regress/regress1/fmf/am-bad-model.cvc | 23 |
1 files changed, 0 insertions, 23 deletions
diff --git a/test/regress/regress1/fmf/am-bad-model.cvc b/test/regress/regress1/fmf/am-bad-model.cvc deleted file mode 100644 index 66be7e66f..000000000 --- a/test/regress/regress1/fmf/am-bad-model.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% COMMAND-LINE: -% 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; - |