From f4a082d01dff58bebe1714e29ee1a9916454f435 Mon Sep 17 00:00:00 2001 From: Ari Zerner Date: Sat, 4 Jul 2020 04:25:13 -0400 Subject: [PATCH] Bug fix --- src/main.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main.ml b/src/main.ml index 99c502c..e3da67f 100755 --- a/src/main.ml +++ b/src/main.ml @@ -543,7 +543,7 @@ let run file ((es, gs) as input) = let timer = Timer.start () in check_order_params [Lit.terms e | e <- es @ gs]; let ans, proof = - if gs = [] && !settings.unfailing && not !settings.complete_if_no_goal then + if gs = [] && !settings.unfailing && not !settings.complete_if_no_goal && not !Settings.interactive then (SAT, GroundCompletion ([], [], Order.default)) else if !settings.modulo_ac then Ckb_AC.complete (!settings, !heuristic) (fst input)