summaryrefslogtreecommitdiff
path: root/test
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-07-13 17:36:01 +0200
committerGitHub <noreply@github.com>2018-07-13 17:36:01 +0200
commitc369afa180b7cb3d9388c39d18fcb81e8246ff21 (patch)
tree149026fe09eb96fa338c3869ac7da78f12448a93 /test
parent96dcf80d249ecbf12f1e3a0cd473deade007a1c3 (diff)
sygusComp2018: optimization for collect model info (#2105)
Diffstat (limited to 'test')
-rw-r--r--test/regress/regress0/tptp/DAT001=1.p1
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/regress0/tptp/DAT001=1.p b/test/regress/regress0/tptp/DAT001=1.p
index 922a6cfc3..f30db563a 100644
--- a/test/regress/regress0/tptp/DAT001=1.p
+++ b/test/regress/regress0/tptp/DAT001=1.p
@@ -1,3 +1,4 @@
+% COMMAND-LINE: --no-finite-model-find
%------------------------------------------------------------------------------
% File : DAT001=1 : TPTP v5.5.0. Released v5.0.0.
% Domain : Data Structures
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback