diff --git a/paynt/parser/sketch.py b/paynt/parser/sketch.py index 27a8e528..44478833 100644 --- 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 index 2f3c722b..c351c8dd 100644 --- 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; }