From 3ec4f6f2e328d40543d38636297243ea9d1efed4 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Mon, 9 Feb 2015 14:15:15 +0100 Subject: [PATCH] [bugfix] semantic backtrack added decision with wrong level --- solver/mcsolver.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml index 1c7e6c3a..3818b0d7 100644 --- a/solver/mcsolver.ml +++ b/solver/mcsolver.ml @@ -445,7 +445,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S) else begin env.decisions <- env.decisions + 1; new_decision_level(); - enqueue_bool fuip.neg blevel (Bcp None) + enqueue_bool fuip.neg (decision_level ()) (Bcp None) end end; var_decay_activity ();