change default valuations file

randriu · Oct 10, 2024 · 80124e9 · 80124e9
1 parent efcc202
commit 80124e9
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/paynt/parser/sketch.py b/paynt/parser/sketch.py
@@ -88,13 +88,14 @@ def load_sketch(cls, sketch_path, properties_path,
                 specification = PrismParser.parse_specification(properties_path, relative_error)
                 filetype = "drn"
                 project_path = os.path.dirname(sketch_path)
-                valuations_path = project_path + "/state_valuations.json"
+                valuations_filename = "state-valuations.json"
+                valuations_path = project_path + "/" + valuations_filename
                 state_valuations = None
                 if os.path.exists(valuations_path) and os.path.isfile(valuations_path):
                     with open(valuations_path) as file:
                         state_valuations = json.load(file)
                 if state_valuations is not None:
-                    logger.info(f"found state_valuations.json, adding to the model...")
+                    logger.info(f"found state valuations in {valuations_path}, adding to the model...")
                     explicit_quotient = payntbind.synthesis.addStateValuations(explicit_quotient,state_valuations)
             except Exception as e:
                 print(e)

diff --git a/payntbind/src/synthesis/quotient/TreeNode.cpp b/payntbind/src/synthesis/quotient/TreeNode.cpp
@@ -453,7 +453,6 @@ bool InnerNode::isPathEnabledInState(
 ) const {
     bool step_to_true_child = path[depth];
     for(uint64_t variable = 0; variable < numVariables(); ++variable) {
-        z3::expr const& dv = decision_hole.solver_variable;
         if(not subfamily.holeContains(decision_hole.hole,variable)) {
             continue;
         }