summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sygus/General_plus10.sy
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-02-02 17:20:44 -0600
committerGitHub <noreply@github.com>2018-02-02 17:20:44 -0600
commitae5c1a5c3a9c6eb7d1af1a4ddbcb841cf7ce4c70 (patch)
tree3d8fe399ff6a6dd6ac7cf119b422cc1d5ea5604d /test/regress/regress0/sygus/General_plus10.sy
parent73a92766063e76e6c6f2507f126fb8f84ed3e432 (diff)
Fix remaining synthesis solution regressions (#1557)
Diffstat (limited to 'test/regress/regress0/sygus/General_plus10.sy')
-rwxr-xr-xtest/regress/regress0/sygus/General_plus10.sy2
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress0/sygus/General_plus10.sy b/test/regress/regress0/sygus/General_plus10.sy
index 33552f9e2..1792749e2 100755
--- a/test/regress/regress0/sygus/General_plus10.sy
+++ b/test/regress/regress0/sygus/General_plus10.sy
@@ -1,5 +1,5 @@
; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status --no-check-synth-sol
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
(set-logic LIA)
(synth-fun fb () Int ((Start Int ((Constant Int)))))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback