summaryrefslogtreecommitdiff
path: root/contrib/run-script-cascj7-fnt
diff options
context:
space:
mode:
authorajreynol <reynolds@laraserver2.epfl.ch>2014-05-28 23:32:59 +0200
committerajreynol <reynolds@laraserver2.epfl.ch>2014-05-28 23:32:59 +0200
commitd38ad982be4717eee4fa102533e12c338b2d1b37 (patch)
tree62ca2dcf4f7889bfe432563508b5e3e22e2bf3fc /contrib/run-script-cascj7-fnt
parentb8bd234936a499d72cb5a9444f8cfd82d980fe8f (diff)
Minor changes to script. Disable cbqi sat.
Diffstat (limited to 'contrib/run-script-cascj7-fnt')
-rwxr-xr-xcontrib/run-script-cascj7-fnt2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/run-script-cascj7-fnt b/contrib/run-script-cascj7-fnt
index ce54fe5ae..0d8642e67 100755
--- a/contrib/run-script-cascj7-fnt
+++ b/contrib/run-script-cascj7-fnt
@@ -15,7 +15,7 @@ echo "------- cvc4-fnt casc j7 : $bench at $2..."
function trywith {
limit=$1; shift;
echo "--- Run $@ at $limit...";
- (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
+ (ulimit -S -t "$limit";$cvc4 --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null |
(read w1 w2 w3 result w4 w5;
case "$result" in
Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback