From 75bbe18a3f8f7b814a7716574fd3619bf69ba85b Mon Sep 17 00:00:00 2001 From: yoni206 Date: Tue, 17 Jul 2018 14:20:46 -0700 Subject: Refactor sep-pre-skolem-emp preprocessing pass --- test/regress/regress0/sep/skolem_emp.smt2 | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 test/regress/regress0/sep/skolem_emp.smt2 (limited to 'test/regress/regress0') diff --git a/test/regress/regress0/sep/skolem_emp.smt2 b/test/regress/regress0/sep/skolem_emp.smt2 new file mode 100644 index 000000000..d17f98ac3 --- /dev/null +++ b/test/regress/regress0/sep/skolem_emp.smt2 @@ -0,0 +1,5 @@ +; COMMAND-LINE: --no-check-models --sep-pre-skolem-emp +; EXPECT: sat +(set-logic QF_ALL_SUPPORTED) +(assert (not (emp 0 0))) +(check-sat) -- cgit v1.2.3