From 5b4c416608bda1df62e1ffe7131648a89882ddc7 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Tue, 30 Oct 2012 23:22:07 +0000 Subject: [PATCH] delta of a model-building failure case --- test/regress/regress0/uflra/Makefile.am | 2 ++ test/regress/regress0/uflra/incorrect1.delta02.smt | 14 ++++++++++++++ 2 files changed, 16 insertions(+) create mode 100644 test/regress/regress0/uflra/incorrect1.delta02.smt diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index 57c56c01b..289569b1a 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -33,6 +33,8 @@ SMT_TESTS = \ pb_real_10_0200_10_29.smt \ incorrect2.smt \ incorrect1.smt \ + incorrect1.delta01.smt \ + incorrect1.delta02.smt error1.smt # Regression tests for SMT2 inputs diff --git a/test/regress/regress0/uflra/incorrect1.delta02.smt b/test/regress/regress0/uflra/incorrect1.delta02.smt new file mode 100644 index 000000000..9d9d65edc --- /dev/null +++ b/test/regress/regress0/uflra/incorrect1.delta02.smt @@ -0,0 +1,14 @@ +(benchmark fuzzsmt +:logic QF_UFLRA +:extrafuns ((f1 Real Real Real)) +:status sat +:formula +(let (?n1 6) +(let (?n2 (~ ?n1)) +(let (?n3 (/ ?n1 ?n2)) +(let (?n4 1) +(let (?n5 (+ ?n3 ?n4)) +(let (?n6 (f1 ?n4 ?n4)) +(flet ($n7 (distinct ?n5 ?n6)) +$n7 +)))))))) -- 2.30.2