diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-12 19:21:30 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-06-12 19:21:30 +0000 |
commit | a450fbb38547d42fe618b325b06a4aff430dd378 (patch) | |
tree | e572730da1bd2a423a62dc5b03916f746b500245 /test/regress/regress0/uflia | |
parent | c58fa3ff70a1bb6b13ef9489159a899c4f49b004 (diff) |
Assert fail equaility_engine.cpp: hasTerm(node) with --decision=justification
Diffstat (limited to 'test/regress/regress0/uflia')
-rw-r--r-- | test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta05.smt | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta05.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta05.smt new file mode 100644 index 000000000..23e4ba01f --- /dev/null +++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta05.smt @@ -0,0 +1,18 @@ +(benchmark mathsat +:logic QF_UFLIA +:extrafuns ((select_format Int Int)) +:extrafuns ((adr_lo Int)) +:extrafuns ((arg1 Int)) +:status unknown +:formula +(let (?n1 (select_format arg1)) +(flet ($n2 (= ?n1 adr_lo)) +(let (?n3 0) +(flet ($n4 (= adr_lo ?n3)) +(let (?n5 1) +(let (?n6 (select_format ?n5)) +(flet ($n7 (= adr_lo ?n6)) +(flet ($n8 (or $n4 $n7)) +(flet ($n9 (and $n2 $n8)) +$n9 +)))))))))) |